Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results
| dc.contributor.author | Bultan, Tevfik | en_US |
| dc.contributor.author | Gerber, Richard | en_US |
| dc.contributor.author | Pugh, William | en_US |
| dc.date.accessioned | 2004-05-31T22:49:44Z | |
| dc.date.available | 2004-05-31T22:49:44Z | |
| dc.date.created | 1998-02 | en_US |
| dc.date.issued | 1998-10-15 | en_US |
| dc.description.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) | en_US |
| dc.format.extent | 447733 bytes | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.uri | http://hdl.handle.net/1903/936 | |
| dc.language.iso | en_US | |
| dc.relation.isAvailableAt | Digital Repository at the University of Maryland | en_US |
| dc.relation.isAvailableAt | University of Maryland (College Park, Md.) | en_US |
| dc.relation.isAvailableAt | Tech Reports in Computer Science and Engineering | en_US |
| dc.relation.isAvailableAt | UMIACS Technical Reports | en_US |
| dc.relation.ispartofseries | UM Computer Science Department; CS-TR-3870 | en_US |
| dc.relation.ispartofseries | UMIACS; UMIACS-TR-98-07 | en_US |
| dc.title | Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results | en_US |
| dc.type | Technical Report | en_US |