Predicate Abstraction using SAT

About SATABS

SATABS is a verification tool for ANSI-C and C++ programs. SATABS trans­forms 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 ab­strac­tion is best suited for lightweight properties such as array bounds (buffer over­flows), 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, con­tact Daniel Kroening. You should also read the license.

Documentation

• The SATABS manual gives a tutorial from a user's point of view and describes what pro­perties are checked.

• A set of slides on SATABS: PDF, 2x3 handouts

• Tutorials

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

 

SATABS Screenshots

   
Click to enlarge.