Predicate abstraction with indexed predicates

DOI10.1145/1297658.1297662MaRDI QIDQ5277793zbMATH OpenOpenAlexFDO

Authors Shuvendu K. Lahiri, Randal E. Bryant

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/0407006

zbMATH Keywords

abstract interpretationcache-coherence protocolsformal verificationinfinite-state verificationinvariant synthesispredicate abstraction

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Predicate abstraction with minimum predicates
• Predicate abstraction in a program logic calculus
• Predicate Abstraction in a Program Logic Calculus
• Predicate abstraction for linked data structures
• Predicate abstraction of rewrite theories
• scientific article; zbMATH DE number 2102703
• Predicate Abstraction with Under-approximation Refinement
• Predicate Abstraction via Symbolic Decision Procedures
• Computer Aided Verification

Cited in

(14)

• Verification of SpecC using predicate abstraction
• Pre-indexed Terms for Prolog
• Abstract Counterexamples for Non-disjunctive Abstractions
• scientific article; zbMATH DE number 1979540 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• Predicate abstraction of rewrite theories
• Predicate Abstraction via Symbolic Decision Procedures
• Computer Aided Verification
• Automated Technology for Verification and Analysis
• Predicate abstraction in a program logic calculus
• MCMT: a model checker modulo theories
• A symbolic approach to predicate abstraction.
• Verification, Model Checking, and Abstract Interpretation
• Invariant checking for SMT-based systems with quantifiers

This page was built for publication: Predicate abstraction with indexed predicates

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277793)