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

Affine invariantsClausal invariantsInvariant generationModel checkingPolynomial invariantsStatic analysis

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

• A technique for invariant generation
• 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

• 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
• Applications of Craig interpolants in model checking
• Applying SAT methods in unbounded symbolic model checking
• Atsuji completions vis-à-vis hyperspaces
• Automatic abstraction without counterexamples
• 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
• Constraint-based linear-relations analysis
• Counterexample-guided abstraction refinement
• scientific article; zbMATH DE number 4089320 (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?)
• Hybrid Systems: Computation and Control
• Interpolation and SAT-based model checking.
• Introduction to set constraint-based program analysis
• Linear ranking with reachability
• Petri net analysis using invariant generation
• Practical methods for proving program termination
• Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming
• SAT-based induction for temporal safety properties
• Scalable analysis of linear systems using mathematical programming
• Structured and simultaneous Lyapunov functions for system stability problems
• Symbolic model checking: \(10^{20}\) states and beyond
• Synthesis of linear ranking functions
• Termination criteria for bounded model checking: extensions and comparison
• Verification Constraint Problems with Strengthening
• Verification, Model Checking, and Abstract Interpretation

Cited in

(24)

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

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)