Model Checking and Static Program Analysis

Current software model-checkers are based on predicate abstraction. Values of variables in branching conditions are represented abstractly using predicates.  The strength of the approach is its control flow based analysis.  However, if the control flow depends heavily on values of memory cells on the heap, the approach does not work well because it cannot find 'good' predicate abstractions to represent the heap content.  Shape analysis -- a modern static program analysis technique -- can lead to a very compact representation of data structures stored on the heap, e.g., lists and trees. However, the data-flow analysis is not path-sensitive and therefore produces many `false-positives', i.e., it reports errors for correct programs. We have combined shape analysis with predicate abstraction, and integrated it into the model checker Blast.

There are two projects in this area:
  1. In a case study, the student will verify several C programs using both techniques, model checking and static analysis, at the same time using the existing implementation of Blast.
  2. In another project, the student will implement an extension of the current static analysis.

Contact: Gregory Theoduloz