Computer Science – Logic in Computer Science
Scientific paper
2004-07-02
Computer Science
Logic in Computer Science
27 pages, 4 figures, 1 table, short version appeared in International Conference on Verification, Model Checking and Abstract
Scientific paper
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.
Bryant Randal E.
Lahiri Shuvendu K.
No associations
LandOfFree
Predicate Abstraction with Indexed Predicates does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Predicate Abstraction with Indexed Predicates, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Predicate Abstraction with Indexed Predicates will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-203640