Sciweavers

SPIN
2007
Springer

SAT-Based Summarization for Boolean Programs

14 years 4 months ago
SAT-Based Summarization for Boolean Programs
Boolean programs are frequently used to model abstractions of software programs. They have the advantage that reachability properties are decidable, despite the fact that their stack is not bounded. The enabling technique is summarization of procedure calls. Most model checking tools for Boolean programs use BDDs to represent these summaries, allowing for an efficient fix-point detection. However, BDDs are highly sensitive to the number of state variables. We present an approach to over-approximate summaries using Bounded Model Checking. Our technique is based on a SAT solver and requires only few calls to a QBF solver for fix-point detection. We present benchmarks that show that our implementation is able handle a larger number of variables than BDD-based algorithms on some examples.
Gérard Basler, Daniel Kroening, Georg Weiss
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where SPIN
Authors Gérard Basler, Daniel Kroening, Georg Weissenbacher
Comments (0)