Model Checking Concurrent Systems with Unbounded Integer Variables:
Symbolic Representations, Approximations and Experimental Results
Model Checking Concurrent Systems with Unbounded Integer Variables:
Symbolic Representations, Approximations and Experimental Results
Files
Publication or External Link
Date
1998-10-15
Authors
Bultan, Tevfik
Gerber, Richard
Pugh, William
Advisor
Citation
DRUM DOI
Abstract
Model checking is a powerful technique for analyzing large, finite-state
systems. In an infinite-state system, however, many basic properties are
undecidable. In this paper, we present a new symbolic model checker which
conservatively evaluates safety and liveness properties on infinite-state
programs. We use Presburger formulas to symbolically encode a program's
transition system, as well as its model-checking computations. All
fixpoint
calculations are executed symbolically, and their convergence is
guaranteed
by using approximation techniques. We demonstrate the promise of this
technology on some well-known infinite-state concurrency problems.
(Also cross-referenced as UMIACS-TR-98-07)