Show simple item record

dc.contributor.authorBultan, Tevfiken_US
dc.contributor.authorGerber, Richarden_US
dc.contributor.authorPugh, Williamen_US
dc.date.accessioned2004-05-31T22:49:44Z
dc.date.available2004-05-31T22:49:44Z
dc.date.created1998-02en_US
dc.date.issued1998-10-15en_US
dc.identifier.urihttp://hdl.handle.net/1903/936
dc.description.abstractModel 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.extent447733 bytes
dc.format.mimetypeapplication/postscript
dc.language.isoen_US
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3870en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-98-07en_US
dc.titleModel Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Resultsen_US
dc.typeTechnical Reporten_US
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.relation.isAvailableAtTech Reports in Computer Science and Engineeringen_US
dc.relation.isAvailableAtUMIACS Technical Reportsen_US


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record