Property-directed incremental invariant generation
DOI10.1007/S00165-008-0080-9zbMATH Open1149.68402OpenAlexW1973291036MaRDI QIDQ939166FDOQ939166
Authors: 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
Recommendations
Model checkingStatic analysisInvariant generationAffine invariantsClausal invariantsPolynomial invariants
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Title not available (Why is that?)
- Hybrid Systems: Computation and Control
- Symbolic model checking: \(10^{20}\) states and beyond
- A lattice-theoretical fixpoint theorem and its applications
- Title not available (Why is that?)
- Analysis of Non-polynomial Systems Using the Sum of Squares Decomposition
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interpolation and SAT-based model checking.
- Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
- Affine relationships among variables of a program
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Termination criteria for bounded model checking: extensions and comparison
- Verification Constraint Problems with Strengthening
- Title not available (Why is that?)
- Title not available (Why is that?)
- Static Analysis
- Verification, Model Checking, and Abstract Interpretation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Introduction to set constraint-based program analysis
- Structured and simultaneous Lyapunov functions for system stability problems
- Computer Aided Verification
- SAT-based induction for temporal safety properties
- Atsuji completions vis-à-vis hyperspaces
- Computational experience with the reverse search vertex enumeration algorithm
- Petri net analysis using invariant generation
Cited In (23)
- Strengthening invariants for efficient computation
- On invariant checking
- A deductive approach towards reasoning about algebraic transition systems
- On the query complexity of selecting minimal sets for monotone predicates
- Property directed equivalence via abstract simulation
- Extending Sledgehammer with SMT solvers
- From invariant checking to invariant inference using randomized search
- Semi-intelligible Isar proofs from machine-generated proofs
- Propositional SAT solving
- Minimal sets on propositional formulae. Problems and reductions
- Software verification with PDR: an implementation of the state of the art
- On invariant synthesis for parametric systems
- Backward symbolic execution with loop folding
- Property-directed inference of universal invariants or proving their absence
- Sledgehammer: judgement day
- When is a formula a loop invariant?
- Learning inductive invariants by sampling from frequency distributions
- Extending Sledgehammer with SMT solvers
- Title not available (Why is that?)
- Strengthening induction-based race checking with lightweight static analysis
- Property-directed inference of universal invariants or proving their absence
- Goal-directed invariant synthesis for model checking modulo theories
- \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants
Uses Software
This page was built for publication: Property-directed incremental invariant generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q939166)
