2005 | OriginalPaper | Buchkapitel
SATABS: SAT-Based Predicate Abstraction for ANSI-C
verfasst von : Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.