Home | Impressum | Sitemap | KIT

Automatic Program Checking

Automatic Program Checking
Typ: lecture Links:
Semester: SS 2010

Geb. 50. 34, Room 236


Mon. and Thu. 14:00 - 15:30

Beginn: Monday 12.04.2010

Mana Taghdiri, Aboubakr Achraf El Ghazi

SWS: 3

The goal of this course is to introduce students to some modern approaches that can
simplify the software development process. We will describe a number of program
checking techniques, explain their pros and cons, and discuss what else needs to be
done in order to make them fully applicable to real-life software systems.

In this lecture, we will cover some state-of-the-art techniques that check and detect
correctness properties of programs. We will particularly focus on lightweight tech-
niques that work at a push-of-a-button: those that are fully automatic and expect
very little input from users. Because these techniques do not depend on much user-
provided guidance and can be run without any user interactions, they can be easily
incorporated into a wide range of software development processes.

In this lecture, we will cover techniques for:

  • Generating test cases exhaustively,
  • Generating test cases randomly,
  • Finding bugs in object-oriented programs,
  • Summarizing programs’ behavior,
  • Detecting invariants about programs,
  • Designing feedback loops for analyzing large programs.


  • Alloy:
    • Alloy website: http://alloy.mit.edu/community
    • Software abstractions: logic, language, and analysis, D. Jackson, MIT Press, Cambridge, MA, March 2006. (dy amazon)
    • A comparison of object modeling notations: Alloy, UML, and Z, D. Jackson, 1999.  (pdf)
    • A micromodularity mechanism, D. Jackson, I. Shlyakhter, M. Sridharan, 2001. (pdf)
    • Agile specifications, D. Rayside, A. Milicevic, K. Yessenov, G. Dennis, D. Jackson, 2009. (pdf)
    • Automatic visualization of relational logic models, D. Rayside, F. Chang, G. Dennis, R. Seater, D. Jackson, 2007. (pdf)
  • Alloy Engine:
    • Automating first-order relational logic, D. Jackson, 2000. (pdf)
    • Generating effective symmetry-breaking predicates for search problems, I. Shlyakhter, 2001. (pdf)
    • Exploiting subformula sharing in automatic analysis of quantified formulas, I. Shlyakhter, M. Sridharan, R. Seater, D. Jackson, 2003. (pdf)
    • Kodkod: a relational model finder, E. Torlak, D. Jackson, 2007. (pdf)
    • Kodkod for Alloy users, E. Torlak, G. Dennis, 2006. (pdf)
  • Test case generation :
    • TestEra Generating Structurally Complex Tests from Declarative Constraints, S. Khurshid, MIT PhD Thesis, 2003. (pdf)
    • Korat Automatic Testing of Software with Structurally Complex Inputs, D. Marinov, MIT PhD Thesis, 2004. (pdf)
    • Randoop Directed Random Testing, C. Pacheco, MIT PhD Thesis, 2009. (pdf)
    • Cute  Scalable Automated Methods for Dynamic Program Analysis, K. Sen, UIUC PhD Thesis , 2006. (pdf)
  • Static bug finding:
    • Jalloy Finding Bugs in Software with a Constraint Solver, M. Vaziri, MIT PhD Thesis, 2004. (pdf)
    • Forge Modular verification of code with SAT, G. Dennis, F. Chang, D. Jackson, 2006. (pdf)
    • A Case for Using Data-flow Analysis to Optimize Incremental Scope-bounded Checking, D. Shao, D. Gopinath, S. Khurshid, and D. Perry, 2010. (pdf)
    • An incremental approach to scope-bounded checking using a lightweight formal method, D. Shao, S. Khurshid, D. Perry, 2009. (pdf)
    • ESC/Java  Extended static checking for Java, C. Flanagan, R. Leino, et. al., 2002. (pdf)
  • Invariant detection:
    • Houdini, an annotation assistant for ESC/Java, C. Flanagan, R. Leino, 2001. (pdf)
    • Daikon Dynamically discovering likely program invariants, M. Ernst, UW PhD thesis, 2000. (pdf)
    • Lightweight Extraction of Syntactic Specifications, M. Taghdiri, 2006. (pdf)