Property-directed incremental invariant generation

DOI10.1007/s00165-008-0080-9zbMath1149.68402OpenAlexW1973291036MaRDI QIDQ939166

Aaron R. Bradley, Zohar Manna

Publication date: 21 August 2008

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-008-0080-9

zbMATH Keywords

Static analysisModel checkingInvariant generationAffine invariantsClausal invariantsPolynomial invariants

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (15)

Software Verification with PDR: An Implementation of the State of the Art ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Propositional SAT Solving ⋮ Backward symbolic execution with loop folding ⋮ A deductive approach towards reasoning about algebraic transition systems ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ When Is a Formula a Loop Invariant? ⋮ On invariant checking ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Sledgehammer: Judgement Day ⋮ Extending Sledgehammer with SMT Solvers ⋮ Strengthening Induction-Based Race Checking with Lightweight Static Analysis ⋮ On invariant synthesis for parametric systems ⋮ Extending Sledgehammer with SMT solvers ⋮ On the query complexity of selecting minimal sets for monotone predicates

Uses Software

• Mathematica
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• Affine relationships among variables of a program
• Introduction to set constraint-based program analysis
• A lattice-theoretical fixpoint theorem and its applications
• Atsuji completions vis-à-vis hyperspaces
• Verification Constraint Problems with Strengthening
• Analysis of Non-polynomial Systems Using the Sum of Squares Decomposition
• Structured and simultaneous Lyapunov functions for system stability problems
• Computational experience with the reverse search vertex enumeration algorithm
• Verification: Theory and Practice
• Hybrid Systems: Computation and Control
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Property-directed incremental invariant generation