Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results

Loading...
Thumbnail Image

Files

CS-TR-3870.ps (437.24 KB)
No. of downloads: 128
1032.pdf (403.58 KB)
No. of downloads: 1139

Publication or External Link

Date

1998-10-15

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)

Notes

Rights