A Model Checker based on Abstraction Refinement
Andrey Rybalchenko, Andreas Podelski, Reinhard Wilhelm · Max Planck Institute for Plasma Physics · 2002
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.