SATABS: SAT-Based Predicate Abstraction for ANSI-C

SAT-based Predicate Abstraction for ANSI-C Edmund Clarke1 Daniel Kroening2 Natasha Sharygina1,3 Karen Yorav4 1 Carnegie Mellon University, School of Computer Science 2 ETH Zuerich, Switzerland 3 Carnegie Mellon University, Software Engineering Institute 4 IBM, Haifa, Israel This paper presents a model checking tool, SatAbs, that ts 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.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav
• Keywords: Algorithms, Carnegie Mellon University, Predicate Abstraction, SAT-based Predicate Abstraction, TACAS 2005