Advertisement
Published in:
2005 | OriginalPaper | Chapter
SATABS: SAT-Based Predicate Abstraction for ANSI-C
Authors : Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
Published in: Tools and Algorithms for the Construction and Analysis of Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.