This paper presents a model checking tool, SATABS, that implements a predicate abstraction refinement loop. Existing software verification tools such as SLAM, BLAST, or MAGIC use decision procedures for abstraction and simulation that are limited to integers. SATABS overcomes these limitations by using a SAT-solver. This allows the model checker to handle the semantics of the ANSI-C standard accurately. This includes a sound treatment of bit-vector overflow, and of the ANSI-C pointer arithmetic constructs. As done by existing tools, SATABS allows checking user-specified assertions, and due to its increased accuracy, to check the correctness of the pointer and array constructs. In addition to that, the tool can also be used to check consistency of C programs with hardware descriptions given in Verilog.
To Appear in Proceedings of the Tools and Agorithms for Construction and Analysis (TACAS) 2005 Conference, 4 pages.
© 2005 Natasha Sharygina.