Symbolic Model Checking of Infinite State Programs Using Presburger Artihmetic
| 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:41:21Z | |
| dc.date.available | 2004-05-31T22:41:21Z | |
| dc.date.created | 1996-09 | 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 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) | en_US |
| dc.format.extent | 279892 bytes | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.uri | http://hdl.handle.net/1903/845 | |
| 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-3687 | en_US |
| dc.relation.ispartofseries | UMIACS; UMIACS-TR-96-66 | en_US |
| dc.title | Symbolic Model Checking of Infinite State Programs Using Presburger Artihmetic | en_US |
| dc.type | Technical Report | en_US |