SATABS Predicate Abstraction using SAT


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.


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.


We also provide papers that describe how SATABS works.



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

x86 Windows x86 Linux
    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

SATABS Screenshots

screenshot  screenshot 
Click to enlarge.


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