A Model Checker based on Abstraction Refinement

1.0

Abstraction plays an important role for verification of computer
programs. We want to construct the right abstraction automatically.
There is a promising approach to do it, called {\it predicate abstraction}.
An insufficiently precise abstraction can be {\it automatically refined}.
There is an automated model checking method described in
[Ball, Podelski, Rajamani TACAS02] which combines both techniques,
e.g., predicate abstraction and abstraction refinement. The quality of
the method is expressed by a completeness property relative to a
powerful but unrealistic oracle-guided algorithm.
\par
In this work we want to generalize the results from
[Ball,Podelski,Rajamani TACAS02] and introduce new abstraction
functions with different precision. We implement the new
abstraction functions in a model checker and practically evaluate
their effectiveness in verifying various computer programs.

Software Model Checking, Verification, Abstraction, Abstract Interpretation, Predicate Abstraction, Refinement

April

2024