Verifying Systems with Integer Constraints and Boolean Predicates: A
Composite Approach
Verifying Systems with Integer Constraints and Boolean Predicates: A
Composite Approach
No Thumbnail Available
Files
Publication or External Link
Date
1998-10-15
Authors
Bultan, Tevfik
Gerber, Richard
League, Christopher
Advisor
Citation
DRUM DOI
Abstract
Symbolic model checking has proved highly successful for large
finite-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 infinite 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 verified some
subtle, infinite-state concurrency problems, it proved inefficient 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 effectiveness on a
nontrivial requirements specification, which includes a mixture of
Booleans, integers and enumerated types.
(Also cross-referenced as UMIACS-TR-97-62)