Predicate Abstaction 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.

SATABS is built in collaboration with Natasha Sharygina. For questions about SATABS, con­tact Daniel Kroening. You should also read the license.

Documentation

From a user's point of view, the SATABS manual gives a tutorial and describes what pro­perties are checked.

• Supported Language Features
• SATABS Manual (PDF)
• Examples and Tutorials

We also provide papers that describe how SATABS works.

• 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

Doina Bucur has built an instrumentor to check programs written for TinyOS.

 

SATABS Screenshots

   
Click to enlarge.