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.

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: Gérard Basler, Daniel Kroening, Georg Weissenbacher
• Keywords: Boolean Programs, Model Checking, SPIN 2007, Theoretical Computer Science, fix-point Detection