Property-directed incremental invariant generation

DOI10.1007/S00165-008-0080-9MaRDI QIDQ939166zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

Model checkingStatic analysisInvariant 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)

Recommendations

• scientific article; zbMATH DE number 1701754
• Goal-directed invariant synthesis for model checking modulo theories
• Property-directed inference of universal invariants or proving their absence
• Computer Aided Verification
• Property-directed inference of universal invariants or proving their absence

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• scientific article; zbMATH DE number 1903370 (Why is no real title available?)
• scientific article; zbMATH DE number 868107 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Affine relationships among variables of a program
• Analysis of Non-polynomial Systems Using the Sum of Squares Decomposition
• Atsuji completions vis-à-vis hyperspaces
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Computational experience with the reverse search vertex enumeration algorithm
• Computer Aided Verification
• Computer Aided Verification
• Hybrid Systems: Computation and Control
• Interpolation and SAT-based model checking.
• Introduction to set constraint-based program analysis
• Petri net analysis using invariant generation
• SAT-based induction for temporal safety properties
• Static Analysis
• Structured and simultaneous Lyapunov functions for system stability problems
• Symbolic model checking: \(10^{20}\) states and beyond
• Termination criteria for bounded model checking: extensions and comparison
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification Constraint Problems with Strengthening
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(23)

• Strengthening invariants for efficient computation
• From invariant checking to invariant inference using randomized search
• Propositional SAT solving
• Extending Sledgehammer with SMT solvers
• Sledgehammer: judgement day
• On invariant checking
• Semi-intelligible Isar proofs from machine-generated proofs
• When is a formula a loop invariant?
• A deductive approach towards reasoning about algebraic transition systems
• Software verification with PDR: an implementation of the state of the art
• Learning inductive invariants by sampling from frequency distributions
• On invariant synthesis for parametric systems
• \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants
• On the query complexity of selecting minimal sets for monotone predicates
• scientific article; zbMATH DE number 1701754 (Why is no real title available?)
• Property-directed inference of universal invariants or proving their absence
• Strengthening induction-based race checking with lightweight static analysis
• Extending Sledgehammer with SMT solvers
• Minimal sets on propositional formulae. Problems and reductions
• Backward symbolic execution with loop folding
• Property-directed inference of universal invariants or proving their absence
• Property directed equivalence via abstract simulation
• Goal-directed invariant synthesis for model checking modulo theories

Describes a project that uses

Uses Software

• Mathematica
• Chaff

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)