Model Checking and Static Program AnalysisCurrent
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:
- 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.
- In another project, the student will implement an extension of the current static analysis.