Predicate abstraction with indexed predicates

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.

• Publication year

  2004

• Venue

  TOCL

• Publication date

  2004-07-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1297658.1297662arXiv cs/0407006
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Indexed Predicate Discovery for Unbounded System Verification

  2004cited by this paper
• Unbounded system verification using decision procedure and predicate abstraction

  2004cited by this paper
• Constructing Quantified Invariants via Predicate Abstraction

  2004cited by this paper
• Modular verification of software components in C

  2004cited by this paper
• Abstract Regular Model Checking

  2004cited by this paper
• A Symbolic Approach to Predicate Abstraction

  2003cited by this paper
• Exact and Efficient Verification of Parameterized Cache Coherence Protocols

  2003cited by this paper
• Modular verification of software components in C

  2003cited by this paper
• Ad hoc On-Demand Distance Vector (AODV) Routing

  2003influential reference
• Modeling and Verification of Out-of-Order Microprocessors in UCLID

  2002cited by this paper
• Deciding Separation Formulas with SAT

  2002cited by this paper
• Predicate abstraction for software verification

  2002cited by this paper
• Lazy abstraction

  2002cited by this paper
• Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions

  2002influential reference
• Deciding CLU Logic Formulas via Boolean and Pseudo-Boolean Encodings

  2002influential reference
• Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness

  2002influential reference
• Counter-Example Based Predicate Discovery in Predicate Abstraction

  2002cited by this paper
• Automatic Deductive Verification with Invisible Invariants

  2001cited by this paper
• Automatic predicate abstraction of C programs

  2001cited by this paper
• Automatic Deductive Veri cation with Invisible Invariants

  2001cited by this paper
• Symbolic model checking with rich assertional languages

  2001cited by this paper
• Parameterized Verification with Automatically Computed Inductive Assertions

  2001cited by this paper
• Successive approximation of abstract transition relations

  2001cited by this paper
• Reducing Model Checking of the Many to the Few

  2000cited by this paper
• Induction in Compositional Model Checking

  2000cited by this paper
• Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach

  1999cited by this paper
• Experience with Predicate Abstraction

  1999cited by this paper
• Verifying Systems with Replicated Components in Murϕ

  1999cited by this paper
• Abstract and Model Check While You Prove

  1999cited by this paper
• Verifying Tomasulo's algorithm by refinement

  1999cited by this paper
• Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking

  1998influential reference
• The Classical Decision Problem

  1997cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• Symbolic Model Checking with Rich ssertional Languages

  1997cited by this paper
• Verifying Systems with Replicated Components in Murphi

  1996cited by this paper
• Reasoning about rings

  1995cited by this paper
• Automatic verification of Pipelined Microprocessor Control

  1994cited by this paper
• Reasoning about systems with many processes

  1992cited by this paper
• Model checking and abstraction

  1992cited by this paper
• Automata on Infinite Objects

  1991cited by this paper
• Limits for Automatic Verification of Finite-State Concurrent Systems

  1986cited by this paper
• Myths About the Mutual Exclusion Problem

  1981cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977influential reference
• Guarded commands, nondeterminacy and formal derivation of programs

  1975cited by this paper
• A new solution of Dijkstra's concurrent programming problem

  1974influential reference
• An illustration.

  1967cited by this paper
• Weak Second‐Order Arithmetic and Finite Automata

  1960cited by this paper
• A New Solution of Dijkstra ' s Concurrent Programming Problem

  year unknowncited by this paper

• Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

  2025cites this paper
• LLM For Loop Invariant Generation and Fixing: How Far Are We?

  2025cites this paper
• Invariant Checking for SMT-Based Systems with Quantifiers

  2024cites this paper
• Regular Abstractions for Array Systems

  2024influential citation
• Ranking LLM-Generated Loop Invariants for Program Verification

  2023cites this paper
• Inferring Inductive Invariants from Phase Structures

  2019cites this paper
• A Framework for the Verification of Parameterized Infinite-state Systems

  2017cites this paper
• Parallel Proofs for Parallel Programs

  2016cites this paper
• Verifying Relative Safety, Accuracy, and Termination for Program Approximations

  2016cites this paper
• Property-Directed Inference of Universal Invariants or Proving Their Absence

  2015cites this paper
• Proof Spaces for Unbounded Parallelism

  2015cites this paper
• A Rule-based Verification Strategy for Array Manipulating Programs

  2015cites this paper
• Automatic program analysis using Max-SMT

  2015cites this paper
• Automated Differential Program Verification for Approximate Computing

  2015cites this paper
• Automatic Verification of Parameterized Systems by Over-Approximation

  2015cites this paper
• Program Verification using Constraint Handling Rules and Array Constraint Generalizations

  2014cites this paper
• Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom

  2014cites this paper
• Proietti A RULE-BASED VERIFICATION STRATEGY FOR ARRAY MANIPULATING PROGRAMS R . 7 2014

  2014cites this paper
• Verifying Array Programs by Transforming Verification Conditions

  2014cites this paper
• Inférence d'invariants pour le model checking de systèmes paramétrés. (Invariants inference for model checking of parameterized systems)

  2014cites this paper
• ICE: A Robust Framework for Learning Invariants

  2014cites this paper
• Secure Virtualization with Formal Methods

  2013cites this paper
• Verification of Imperative Programs by Constraint Logic Program Transformation

  2013cites this paper
• Template-based program verification and program synthesis

  2013cites this paper
• Model checking unbounded concurrent lists

  2013cites this paper
• Universal Guards, Relativization of Quantifiers, and Failure Models in Model Checking Modulo Theories

  2012cites this paper
• Verification with small and short worlds

  2012cites this paper
• Verification of parameterized concurrent programs by modular reasoning about data and control

  2012cites this paper
• SAFARI: SMT-Based Abstraction for Arrays with Interpolants

  2012cites this paper
• Lazy Abstraction with Interpolants for Arrays

  2012cites this paper
• Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms

  2012cites this paper
• State space reduction in modeling checking parameterized cache coherence protocol by two-dimensional abstraction

  2012cites this paper
• A shape analysis for optimizing parallel graph programs

  2011cites this paper
• One step forward: Linking wireless self-organizing network validation techniques with formal testing approaches

  2011cites this paper
• Satisfiability of General Intruder Constraints with and without a Set Constructor

  2011cites this paper
• Model-Checking Parameterized Concurrent Programs Using Linear Interfaces

  2010cites this paper
• Automated Invariant Generation for the Verification of Real-Time Systems

  2010cites this paper
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

  2010cites this paper
• MCMT: A Model Checker Modulo Theories

  2010cites this paper
• Satisfiability-based Program Reasoning and Program Synthesis

  2010influential citation
• Program verification using templates over predicate abstraction

  2009cites this paper
• Abstract Transformers for Thread Correlation Analysis

  2009cites this paper
• Analysis of dynamic evolution systems by spotlight abstraction refinement

  2009cites this paper
• Goal-Directed Invariant Synthesis for Model Checking Modulo Theories

  2009cites this paper
• One step forward : Linking Wireless Self-Organizing Networks Validation Techniques with Formal Testing approaches

  2009cites this paper
• Abstract Counterexamples for Non-disjunctive Abstractions

  2009cites this paper
• Efficiently Inferring Thread Correlations Technical Report TR-09-59203

  2009cites this paper
• Thread Quantification for Concurrent Shape Analysis

  2008cites this paper
• Culling predicates for the Verification of Real-Time Models

  2008cites this paper
• Creating Correct Network Protocols

  2008influential citation
• Formal Verification of Infinite State Systems Using Boolean Methods

  2006cites this paper
• Ad hoc routing protocol validation

  2005cites this paper
• A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures

  2001cites this paper