@inproceedings{lahiri2007predicate,
author = {Lahiri, Shuvendu and Bryant, Randal E.},
title = {Predicate abstraction with indexed predicates},
booktitle = {ACM Transactions on Computational Logic (TOCL '07)},
year = {2007},
month = {January},
abstract = {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.},
publisher = {Association for Computing Machinery, Inc.},
url = {http://approjects.co.za/?big=en-us/research/publication/predicate-abstraction-with-indexed-predicates/},
volume = {9},
edition = {ACM Transactions on Computational Logic (TOCL '07)},
}