Abstractions from proofs
From MaRDI portal
Publication:3452263
DOI10.1145/964001.964021zbMath1325.68147OpenAlexW4212792638MaRDI QIDQ3452263
Rupak Majumdar, Ranjit Jhala, K. L. McMillan, Thomas A. Henzinger
Publication date: 11 November 2015
Published in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/964001.964021
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Proof tree preserving tree interpolation ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ 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 ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Automation of Quantitative Information-Flow Analysis ⋮ Predicate diagrams for the verification of real-time systems ⋮ LCTD: test-guided proofs for C programs on LLVM ⋮ Constraint solving for interpolation ⋮ SMT-based verification of program changes through summary repair ⋮ Verification Modulo theories ⋮ Specifying graph languages with type graphs ⋮ Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction ⋮ SAT-based invariant inference and its relation to concept learning ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ Probabilistic CEGAR ⋮ SAT-based verification for timed component connectors ⋮ Efficient strategies for CEGAR-based model checking ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ Complete instantiation-based interpolation ⋮ Towards the Verification of Attributed Graph Transformation Systems ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Resolution proof transformation for compression and interpolation ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Model checking duration calculus: a practical approach ⋮ Efficient SAT-based bounded model checking for software verification ⋮ On Interpolation in Decision Procedures ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Experience of improving the BLAST static verification tool ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Interpolant Generation for UTVPI ⋮ Ground Interpolation for Combined Theories ⋮ Interpolation and Symbol Elimination ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ Common knowledge does not have the Beth property ⋮ Verifying Reference Counting Implementations ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Automatically Refining Abstract Interpretations ⋮ ExplainHoudini: Making Houdini Inference Transparent ⋮ Distributed and Predictable Software Model Checking ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ View-Augmented Abstractions ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Efficient generation of small interpolants in CNF ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ NIL: learning nonlinear interpolants ⋮ Abstraction Refinement for Quantified Array Assertions ⋮ Refinement of Trace Abstraction ⋮ A Configurable CEGAR Framework with Interpolation-Based Refinements ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ Refining abstract interpretations ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations ⋮ An interpolating theorem prover ⋮ On interpolation in automated theorem proving
