Overview

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!

Projects

Automated Test Generation. Automated techniques for generating tests is a classic research topic that recently has experienced quite a resurgence.

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.

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.

Downloads

• CHESS, systematic testing of multi-threaded programs
• HAVOC, static checker for C code
• Driver Development Kit (contains Static Driver Verifier, based on SLAM)
• Rule Development Kit for SDV (allows you to develop new rules for SLAM)
• Z3 (automated SMT theorem prover)

Alumni

• Jakob Rehof, now Professor at the University of Dortmund and Director, Fraunhofer Institute of Software and Systems Technology

Visitors

• Professors
  • Alfred Aho (2006,2007)
  • Victor R. Basili (2007)
  • Maria Paola Bonacina (2008)
  • Ahmed Bouajjani (2006, 2008)
  • Kousha Etessami (2007)
  • Harald Gall (2008,2009)
  • Ganesh Gopalakrishnan (2009)
  • Thomas Henzinger (2006)
  • Orna Kupferman (2004,2005,2006)
  • Mooly Sagiv (2005)
  • Serdar Tasiran (2005,2006,2007)
  • Andrei Voronkov (2005-2006, 2008)
  • Mihalis Yannakakis (2007)
  • David Walker (2009)
  • Laurie Williams(2009)
  • Andreas Zeller (2005,2009)
• Visiting Researchers
  • Martin Pinzger (2007)
  • Satish Narayanasamy (2007)

Interns

Recruiting Opportunities

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.