swMATH ID: 12804
Software Authors: Clarke, E., Kroning, D., Sharygina, N., Yorav, K.
Description: SATABS: SAT-based predicate abstraction for ANSI-C. This paper presents a model checking tool, SatAbs, that implements a predicate abstraction refinement loop. Existing software verification tools such as Slam, Blast, or Magic use decision procedures for abstraction and simulation that are limited to integers. SatAbs overcomes these limitations by using a SAT-solver. This allows the model checker to handle the semantics of the ANSI-C standard accurately. This includes a sound treatment of bit-vector overflow, and of the ANSI-C pointer arithmetic constructs.
Homepage: http://link.springer.com/chapter/10.1007/978-3-540-31980-1_40
Related Software: BLAST; SLAM; CPAchecker; SPIN; Bebop; CBMC; Zing; UFO; Wolverine; z3; Cogent; KLEE; Orion; DDVerify; SIMPLIFY; Java PathFinder; VCC; CEGAR; ASTREE; FOCI
Referenced in: 35 Publications

Standard Articles

1 Publication describing the Software Year
SatAbs: a bit-precise verifier for C programs (competition contribution)
Basler, Gérard; Donaldson, Alastair; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas

Referencing Publications by Year