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