Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach

Simple item page
dc.contributor.authorBultan, Tevfiken_US
dc.contributor.authorGerber, Richarden_US
dc.contributor.authorLeague, Christopheren_US
dc.date.accessioned2004-05-31T22:47:22Z
dc.date.available2004-05-31T22:47:22Z
dc.date.created1997-08en_US
dc.date.issued1998-10-15en_US
dc.description.abstractSymbolic model checking has proved highly successful for large finite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to systems with an infinite number of states -- even those with a single unbounded integer. Alternatively, we recently proposed a model checker for integer-based systems that uses Presburger constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of Boolean and (unordered) enumerated types -- which possess no natural mapping to the Euclidean coordinate space. In this paper we describe a model checker which combines the strengths of both approaches. We use a composite model, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. We demonstrate our technique's effectiveness on a nontrivial requirements specification, which includes a mixture of Booleans, integers and enumerated types. (Also cross-referenced as UMIACS-TR-97-62)en_US
dc.format.extent236844 bytes
dc.format.mimetypeapplication/postscript
dc.identifier.urihttp://hdl.handle.net/1903/911
dc.language.isoen_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
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3822en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-97-62en_US
dc.titleVerifying Systems with Integer Constraints and Boolean Predicates: A Composite Approachen_US
dc.typeTechnical Reporten_US

Files

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
CS-TR-3822.ps
Size:
231.29 KB
Format:
Postscript Files
Download

Collections

Technical Reports from UMIACS
Technical Reports of the Computer Science Department