Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach

Symbolic model checking has proved highly successful for large nite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to systems with an in nite number of states { even those with a single unbounded integer. Alternatively, we recently proposed a model checker for integer-based systems that uses Presburger constraints as the underlying state representation. While this approach easily veri ed some subtle, in nite-state concurrency problems, it proved ine cient in its treatment of Boolean and (unordered) enumerated types { which possess no natural mapping to the Euclidean coordinate space. In this paper we describe a model checker which combines the strengths of both approaches. We use a composite model, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. We demonstrate our technique's e ect...

• Type: Conference
• Year: 1998
• Where: ISSTA
• Authors: Tevfik Bultan, Richard Gerber, Christopher League
• Keywords: Enumerated Types, ISSTA 1998, Model Checker, Software Engineering, Symbolic Model Checking