Predicate Abstraction with Indexed Predicates
| dc.creator | Lahiri, Shuvendu K. | |
| dc.creator | Bryant, Randal E. | |
| dc.date | 2004-07-02 | |
| dc.date.accessioned | 2026-07-07T03:21:31Z | |
| dc.date.available | 2026-07-07T03:21:31Z | |
| dc.description | Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model checking. We consider models containing first-order state variables, where the system state includes mutable functions and predicates. Such a model can describe systems containing arbitrarily large memories, buffers, and arrays of identical processes. We describe a form of predicate abstraction that constructs a formula over a set of universally quantified variables to describe invariant properties of the first-order state variables. We provide a formal justification of the soundness of our approach and describe how it has been used to verify several hardware and software designs, including a directory-based cache coherence protocol. | |
| dc.description | 27 pages, 4 figures, 1 table, short version appeared in International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), LNCS 2937, pages = 267--281 | |
| dc.identifier | https://arxiv.org/abs/cs/0407006 | |
| dc.identifier | http://arxiv.org/abs/cs/0407006 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/32227 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.3.1 | |
| dc.title | Predicate Abstraction with Indexed Predicates | |
| dc.type | text |