SATABS 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.

SATABS News

New: Version 3.2 for x86 Linux released.

New: see a video of Alastair presenting the use of symmetry in SATABS.

Read the paper!

There is now a Google Group for annoucements related to SATABS.

Documentation

We also provide papers that describe how SATABS works.

 

Download

We distribute binaries for x86 Linux and Windows, and the source via SVN.

x86 Windows x86 Linux
  • SATABS: satabs-3-0-win.zip
    Unzip the archive before running.

  • Important: You need CL (comes with Microsoft Visual Studio) in your PATH for preprocessing. If you don't have Visual Studio, download Visual C++ Express (free!).

  • SATABS: satabs-3-2-linux-32.tgz
    Do tar xfz satabs-3-2-linux-32.tgz before running.

  • The TACAS 2012 competition binary is here: satabs.20111013.2200.tar.bz2

  • Of course, it's assumed that you have gcc/g++ and the usual header files and libraries installed. The archive above comes with Boom.

  • New: Eclipse Plugin for Windows and Linux

  • You need a Model Checker for SATABS. We recommend either Cadence SMV or BOPPO.

  • To get the source of SATABS, do
    svn co http://www.cprover.org/svn/satabs/releases/satabs-3.2

SATABS Screenshots

screenshot  screenshot 
Click to enlarge.

Funding

This research is currently supported by EPSRC grant EP/G026254/1.