Abstractions from proofs
From MaRDI portal
Recommendations
Cited in
(85)- Efficient strategies for CEGAR-based model checking
- Efficient SAT-based bounded model checking for software verification
- Verifying Reference Counting Implementations
- Verification, Model Checking, and Abstract Interpretation
- Interpolation and model checking for nonlinear arithmetic
- AI*IA 2005: Advances in Artificial Intelligence
- Resolution proof transformation for compression and interpolation
- Formal Methods in Computer-Aided Design
- Whale: an interpolation-based algorithm for inter-procedural verification
- Interpolant-Based Transition Relation Approximation
- Abstract Counterexamples for Non-disjunctive Abstractions
- Common knowledge does not have the Beth property
- Abstract Error Projection
- Abstraction Refinement for Quantified Array Assertions
- Proof tree preserving tree interpolation
- Interpolation systems for ground proofs in automated deduction: a survey
- scientific article; zbMATH DE number 1701764 (Why is no real title available?)
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Interpolation and model checking
- SAT-based verification for timed component connectors
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- An extension of lazy abstraction with interpolation for programs with arrays
- Predicate abstraction for program verification
- Interpolation and SAT-based model checking revisited: adoption to software verification
- Guiding Craig interpolation with domain-specific abstractions
- Quantifier-free interpolation in combinations of equality interpolating theories
- Array Abstractions from Proofs
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Experience of improving the BLAST static verification tool
- Distributed and predictable software model checking
- NIL: learning nonlinear interpolants
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- On recursion-free Horn clauses and Craig interpolation
- Lazy Abstraction with Interpolants
- SAT-based invariant inference and its relation to concept learning
- Predicate diagrams for the verification of real-time systems
- Complete instantiation-based interpolation
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- Synthesizing history and prophecy variables for symbolic model checking
- Constraint solving for interpolation
- SMT-based verification of program changes through summary repair
- Efficient generation of small interpolants in CNF
- Model checking duration calculus: a practical approach
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Abstraction and abstraction refinement
- Verification Modulo theories
- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
- Verification and falsification of programs with loops using predicate abstraction
- LCTD: test-guided proofs for C programs on LLVM
- View-augmented abstractions
- Automation of quantitative information-flow analysis
- Refinement of Trace Abstraction
- On interpolation in decision procedures
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- Interpolation and symbol elimination in Vampire
- SAT-Based Model Checking
- Refining abstract interpretations
- Coinductive techniques for checking satisfiability of generalized nested conditions
- Abstraction refinement with Craig interpolation and symbolic pushdown systems
- Parallel program analysis via range splitting
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Abstraction Refinement of Linear Programs with Arrays
- Probabilistic CEGAR
- Abstractions of uniform proofs
- Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
- scientific article; zbMATH DE number 1759674 (Why is no real title available?)
- Learning inductive invariants by sampling from frequency distributions
- Using Abduction to Compute Efficient Proofs
- On interpolation in automated theorem proving
- Quantifier elimination and Craig interpolation: the quantitative way
- Combining model checking and data-flow analysis
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Infinite-state invariant checking with IC3 and predicate abstraction
- An interpolating theorem prover
- Abstraction, Axiomatization and Rigor: Pasch and Hilbert
- Predicate Abstraction in Program Verification: Survey and Current Trends
- ExplainHoudini: making Houdini inference transparent
- Computer Aided Verification
- A configurable CEGAR framework with interpolation-based refinements
- Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
- When are software verification results valid for approximate hardware?
- Automatically Refining Abstract Interpretations
- Towards the Verification of Attributed Graph Transformation Systems
This page was built for publication: Abstractions from proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3452263)
