Predicate Abstraction using SAT
SATABS is a verification tool for ANSI-C and C++ programs. SATABS transforms a C/C++ program into a Boolean program, which is an abstraction of the original program in order to handle large amounts of code. The Boolean program is then passed to a Model Checker. Predicate abstraction is best suited for lightweight properties such as array bounds (buffer overflows), pointer safety, exceptions and control-flow oriented user-specified assertions.
Contributors to SATABS include Alastair Donaldson, Alexander Kaiser, Michael Tautschnig, Natasha Sharygina, Thomas Wahl. For questions about SATABS, contact Daniel Kroening. You should also read the license.
New: Version 3.2 for x86 Linux released.
New: see a video of Alastair presenting the use of symmetry in SATABS.
There is now a Google Group for annoucements related to SATABS.
The SATABS manual gives a tutorial from a user's point of view and describes what properties are checked.
We also provide papers that describe how SATABS works.
- Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs
- Model Checking Concurrent Linux Device Drivers
- SATABS: SAT-based Predicate Abstraction for ANSI-C
- Predicate Abstraction of ANSI-C Programs using SAT
- Verification of SpecC and Verilog using Predicate Abstraction
- Checking Consistency of C and Verilog using Predicate Abstraction and Induction
We distribute binaries for x86 Linux and Windows, and the source via SVN.
This research is currently supported by EPSRC grant EP/G026254/1.