Case Studies in Software Model Checking

Blast is a model checker for C programs: for a given property it computes a counterexample, if the property was violated; or an approximation of the complete state space, if the property holds; or it stops because of time-out. We consider three practical applications of the model checker to software engineering disciplines.

  1. We use the counterexamples to generate test cases for statement and condition coverage. The path-sensitive search in the abstract state space led to a considerable reduction of the set of test cases.
  2. We use the specification language for Blast to define and verify properties of C programs. The specification language supports two levels of abstraction: a monitor automaton describes path-oriented safety properties, and a more abstract location-oriented query language allows for combination of several path-oriented properties.
  3. We apply Blast to proving memory safety of C programs. For example, we can prove if the program contains invalid pointer dereferences. If such a situation is found, Blast reports a path (counterexample) to the location in the program where the memory access violation occurs. 
All three approaches are especially interesting for quality assurance of the software system without manually changing the program source code: the properties of the specification language are specified separately from the source code, test data are fed through the module interface, and memory safety is checked via fully automatic instrumentation of the source code.

For each of the above applications of model checking in software engineering practice, we provide one student project. The student project consists of applying each of the above approaches to a case study, in order to find out for which kind of C programs the method works conveniently.

 Contact: Gregory Theoduloz