SATABS Manual

SATABS – Predicate Abstraction with SAT

Tutorials

We provide an introduction to model checking "real" C programs with SATABS using two small examples:

• An example based on Linux device drivers.
• An example based on a Mail Transfer Agent.