Symbolic Model Checking of Infinite State Programs Using Presburger Artihmetic

Loading...
Thumbnail Image

Files

CS-TR-3687.ps (273.33 KB)
No. of downloads: 247
CS-TR-3687.pdf (270.93 KB)
No. of downloads: 743

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 transition 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-96-66)

Notes

Rights