Reference. AVR: Abstractly Verifying Reachability
We present AVR, a push-button model checker for verifying state transition systems directly at the source-code level. AVR uses information embedded in the word-level syntax of the design representation to automatically perform scalable model checking by combining a novel syntax-guided abstraction-refinement technique with a word-level implementation of the IC3 algorithm. AVR provides independently-verifiable certificates that offer provable assurance and are easy to relate to the word-level system. Moreover, proof certificates can be further used in innovative ways to extract key design information and are useful in a growing number of applications.
Cite
Cited by (2)
Regularity and Quantification: A New Approach to Verify Distributed Protocols goelRegularityQuantificationNew
Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any enumerative search by carefully analyzing the spatial and temporal regularity of the protocol. The key insight underlying this approach is that structural regularity and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components and its unbounded evolution over time. We extended the finite-domain IC3/PDR algorithm to use these regularities and boost clause learning to automatically derive the required quantified inductive invariant by exploiting the connection between structural regularities and quantification. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state-of-the-art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols goelSymmetryQuantificationNew2021
Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any search by carefully analyzing the structural symmetries of the protocol. The key insight underlying this approach is that symmetry and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components. We propose symmetric incremental induction, an extension of the finite-domain IC3/PDR algorithm, that automatically derives the required quantified inductive invariant by exploiting the connection between symmetry and quantification. While various attempts have been made to exploit symmetry in verification applications, to our knowledge, this is the first demonstration of a direct link between symmetry and quantification in the context of clause learning during incremental induction. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state-of-the-art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.
Cites 52 works (3 here)
With notes (3)
I4: Incremental inference of inductive invariants for verification of distributed protocols maI4IncrementalInference2019
Designing and implementing distributed systems correctly is a very challenging task. Recently, formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computerchecked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually—and painstakingly—by the developer. In this paper, we present a new approach, Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of a finite instance of the protocol can be used to infer a general inductive invariant for the infinite distributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC and Transaction Chains with little to no human effort.
Towards Automatic Inference of Inductive Invariants ma-2019-towards
SAT-Based Model Checking without Unrolling bradleySATBasedModelChecking2011
A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.
External (49)
- AVR: Abstractly Verifying Reachability (Zenodo artifact) (2020)
- Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs (2019)
- Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction (2019)
- The SMT Competition (2019)
- Hardware model checking competition (HWMCC) 2019 (2019)
- Efficient verification of multi-property designs (The benefit of wrong assumptions) (2018)
- Btor2 , BtorMC and Boolector (2018)
- Model checking (Clarke, Grumberg, Kroening, Peled, Veith; MIT Press, 2nd ed.) (2018)
- IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language (2017)
- Hardware model checking competition (2017)
- FuseIC3: An algorithm for checking large design spaces (2017)
- ABC: A system for sequential synthesis and verification (2017)
- Hardware Model Checking Competition 2014: An Analysis and Comparison of Model Checkers and Benchmarks (2016)
- Infinite-state invariant checking with IC3 and predicate abstraction (2016)
- Efficient generation of inductive validity cores for safety properties (2016)
- Dependent types and multi-monadic effects in F* (2016)
- The Satisfiability Modulo Theories Library (SMT-LIB) (2016)
- Boolector 2.0 (2015)
- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) (2014)
- IC3 Modulo Theories via Implicit Predicate Abstraction (2014)
- Yices 2.2 (2014)
- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction (2014)
- The MathSAT5 SMT Solver (2013)
- 6 Years of SMT-COMP (2012)
- Efficient implementation of property directed reachability (2011)
- Model checking (2009)
- Scalable and scalably-verifiable sequential synthesis (2008)
- Z3: An Efficient SMT Solver (2008)
- Structural Abstraction of Software Verification Conditions (2007)
- A buffer overflow benchmark for software model checkers (2007)
- Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints (2007)
- BEEM: Benchmarks for Explicit Model Checkers (2007)
- Modelling and solving English Peg Solitaire (2005)
- Applications of Craig Interpolants in Model Checking (2005)
- Automatic abstraction and verification of verilog models (2004)
- Progress on the State Explosion Problem in Model Checking (2001)
- Counterexample-Guided Abstraction Refinement (2000)
- Symbolic Model Checking without BDDs (1999)
- You assume, we guarantee: Methodology and case studies (1998)
- An attack on the Needham-Schroeder public-key authentication protocol (1995)
- Automatic verification of pipelined microprocessor control (1994)
- Why are some problems hard? Evidence from Tower of Hanoi (1985)
- Using encryption for authentication in large networks of computers (1978)
- Apache HTTP server project (website)
- Experiments (github aman-goel/tacas20ae)
- National Vulnerability Database - CVE-2004-0940
- National Vulnerability Database - CVE-2006-3747
- Verification Modulo Theories (vmt-lib.org)
- Yosys open synthesis suite