|
|
Software Reliability Research
|
The Software Reliability Research group studies how program analysis,
program verification and software measurement techniques can be used to
improve the quality of software.
We have made four major releases of our software this past
year. Downloads for
CHESS, HAVOC,
SLAM, and Z3
are now available!
|
|
|
 |
|
Automated Test Generation. Automated techniques for
generating tests is a classic research topic that recently has
experienced quite a resurgence.
- Contact: Patrice
Godefroid
-
Finding Errors in .NET with Feedback-Directed Random Testing,
C. Pacheco, S. K. Lahiri, T. Ball.
To appear,
ISSTA 2008
-
Grammar-based Whitebox Fuzzing, P. Godefroid, A. Kiezun; M
Levin, MSR-TR-2007-154. To appear,
PLDI 2008.
-
Demand-Driven Compositional Symbolic Execution, S. Anand, P.
Godefroid, N. Tillmann.
TACAS
2008
-
Automated Whitebox Fuzz Testing,
P. Godefroid, M. Levin, D. Molnar.
NDSS
2008
|
|
CHESS
is a tool for finding concurrency errors in systems software.
CHESS finds such errors by analyzing executables directly.
|
|
Empirical Software Engineering
activities focus on
understanding various software development issues from an empirical
perspective.
- Contact Nachi
Nagappan
- The Influence of Organizational Structure on Software
Quality, N. Nagappan, B. Murphy, V. Basili.
ICSE 2008
- Predicting Defects using Social Network Analysis on
Dependency Graphs, T. Zimmermann, N. Nagappan.
ICSE 2008
-
The Effect of the Number of Inspectors on the Defect
Estimates Produced by Capture-Recapture Models, G. Walia,
J. Carver, N. Nagappan. ICSE 2008
|
|
HAVOC
is a tool for specifying and checking properties
of systems software written in C. The annotation language of HAVOC
allows the expression of richer properties about the program heap
and data structures such as linked lists and arrays. HAVOC is a
modular verifier.
|
|
SLAM is a joint project with the
RSE group for checking
that software satisfies critical behavioral properties of the
interfaces it uses and to aid software engineers in designing interfaces and
software that ensure reliable and correct functioning.
|
|
Z3 is a new
automated theorem prover (joint project with the FSE
group) supporting linear real and integer arithmetic, fixed-size
bit-vectors, extensional arrays, uninterpreted functions, and
quantifiers. A number of software analysis tools are
building on top of Z3, including Boogie,
Pex,
SAGE, and SLAM.
|
- Goldilocks: Efficiently computing the
happens-before relation using locksets. Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran.
Workshop on Formal Approaches to Testing and Runtime Verification (FATES/RV), 2006.
-
Using Historical In-Process and Product Metrics for Early
Estimation of Software Failures, Nagappan, N.,
Ball, T., Murphy, B.,
Proceedings of the
International Symposium on Software Reliability Engineering,
Raleigh, NC, 2006.
-
Assessing the Relationship between Software
Assertions and Faults: An Empirical Investigation,
Kudrjavets, G., Nagappan, N., Ball., T, Proceedings of the
International Symposium on Software Reliability Engineering,
Raleigh, NC, 2006.
-
Mining Metrics to Predict Component Failures, Nachiappan
Nagappan, Thomas Ball, Andreas Zeller, In the
International
Conference on Software Engineering, Shanghai, China, May
2006.
|
|
- 2007 Interns
- 2006 Interns
- 2005 Interns
- 2004 Interns
|
If you are interested in seeking job opportunities in the SRR research group, please contact
Tom Ball. Also, see the
MSR career site.
We are always looking for exceptional PhD candidates to join us as
interns, any time of the year, though summer is the typical
time interns visit. For more information about
becoming an intern, please visit
our internship website.
|
