Generalized property directed reachability
From MaRDI portal
Recommendations
Cited in
(50)- Automating regression verification of pointer programs by predicate abstraction
- A unifying view on SMT-based software verification
- Relational program reasoning using compiler IR
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Leveraging Horn clause solving for compositional verification of PLC software
- Efficient strategies for CEGAR-based model checking
- Learning inductive invariants by sampling from frequency distributions
- \textsf{PrIC3}: property directed reachability for MDPs
- Unbounded procedure summaries from bounded environments
- Model completeness, covers and superposition
- Infinite-state invariant checking with IC3 and predicate abstraction
- Property directed abstract interpretation
- Understanding IC3
- When is a formula a loop invariant?
- Horn clause solvers for program verification
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Guiding Craig interpolation with domain-specific abstractions
- SAT-Based Model Checking
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Solving constrained Horn clauses using dependence-disjoint expansions
- Tree dimension in verification of constrained Horn clauses
- Parametrized invariance for infinite state processes
- scientific article; zbMATH DE number 7440190 (Why is no real title available?)
- scientific article; zbMATH DE number 7444022 (Why is no real title available?)
- Software verification with PDR: an implementation of the state of the art
- SMT-based verification of data-aware processes: a model-theoretic approach
- SMT-based model checking for recursive programs
- From invariant checking to invariant inference using randomized search
- scientific article; zbMATH DE number 7589540 (Why is no real title available?)
- Improving Generalization in Software IC3
- ICE-based refinement type discovery for higher-order functional programs
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- The Lattice-Theoretic Essence of Property Directed Reachability Analysis
- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
- Simplifying Alternating Automata for Emptiness Testing
- Reasoning About Regular Properties: A Comparative Study
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Exploiting adjoints in property directed reachability analysis
- The \textsc{Golem} Horn solver
- Searching for i-good lemmas to accelerate safety model checking
- Inferring invariants with quantifier alternations: taming the search space explosion
- Property directed reachability for generalized Petri nets
- Antichain with SAT and tries
- \textsc{Golem}: a flexible and efficient solver for constrained Horn clauses
- Adjointness in property directed reachability analysis
- On recursion-free Horn clauses and Craig interpolation
- Generalized property-directed reachability for hybrid systems
- Interpolation and model checking for nonlinear arithmetic
This page was built for publication: Generalized property directed reachability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843329)
