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. ISSTA 2008
• Grammar-based Whitebox Fuzzing, P. Godefroid, A. Kiezun; M Levin, MSR-TR-2007-154. 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.

• Contact: Madan Musuvathi or Shaz Qadeer
• Finding and Reproducing Heisenbugs in Concurrent Programs, M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, I. Neamtiu, To Appear, OSDI 2008
• Effective Program Verification for Relaxed Memory Models. S. Burchkardt, M. Musuvathi. CAV 2008
• Fair Stateless Model Checking, M. Musuvathi, S. Qadeer. MSR-TR 2007-149, 2007. PLDI 2008.

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.

• Contact Shuvendu Lahiri or Shaz Qadeer
• Back to the Future: Revisiting Precise Program Verification using SMT Solvers, S. K. Lahiri, S. Qadeer. POPL 2008
• A Reachability Predicate for Analyzing Low-Level Software, S. Chatterjee, S. K. Lahiri, S. Qadeer and Z. Rakamaric. TACAS 2007
• Verifying Properties of Well-Founded Linked Lists.  POPL 2006

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.

• Contact Thomas Ball or Sriram Rajamani
• Thorough Static Analysis of Device Drivers, T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani and A. Ustuner (Microsoft). EuroSys 2006

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.

• Contact Leonardo de Moura or Nikolaj Bjorner
• Z3: An Efficient SMT Solver, L. de Moura and N. Bjørner. TACAS 2008
• Efficient E-matching for SMT solvers, L. de Moura and Nikolaj Bjørner. CADE 2007
• Model-based Theory Combination, L. de Moura and Nikolaj Bjørner. SMT 2007