Abstractions from proofs
From MaRDI portal
Publication:3452263
DOI10.1145/964001.964021zbMATH Open1325.68147OpenAlexW4212792638MaRDI QIDQ3452263FDOQ3452263
Rupak Majumdar, Ranjit Jhala, Thomas A. Henzinger, K. L. McMillan
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (78)
- Formal Methods in Computer-Aided Design
- Abstract Counterexamples for Non-disjunctive Abstractions
- SAT-based invariant inference and its relation to concept learning
- Synthesizing history and prophecy variables for symbolic model checking
- SMT-based verification of program changes through summary repair
- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction
- Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
- Title not available (Why is that?)
- Using Abduction to Compute Efficient Proofs
- Per-dereference verification of temporal heap safety via adaptive context-sensitive analysis
- When are software verification results valid for approximate hardware?
- Efficient strategies for CEGAR-based model checking
- Verifying Reference Counting Implementations
- Efficient SAT-based bounded model checking for software verification
- Combining Model Checking and Data-Flow Analysis
- Interpolation and model checking for nonlinear arithmetic
- AI*IA 2005: Advances in Artificial Intelligence
- Resolution proof transformation for compression and interpolation
- A Configurable CEGAR Framework with Interpolation-Based Refinements
- ExplainHoudini: Making Houdini Inference Transparent
- Abstract Error Projection
- Automation of Quantitative Information-Flow Analysis
- Common knowledge does not have the Beth property
- Abstraction Refinement for Quantified Array Assertions
- Interpolant Generation for UTVPI
- Title not available (Why is that?)
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Proof tree preserving tree interpolation
- Interpolation systems for ground proofs in automated deduction: a survey
- SAT-based verification for timed component connectors
- Quantifier-free interpolation in combinations of equality interpolating theories
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- An extension of lazy abstraction with interpolation for programs with arrays
- Guiding Craig interpolation with domain-specific abstractions
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Experience of improving the BLAST static verification tool
- Interpolation and Symbol Elimination in Vampire
- NIL: learning nonlinear interpolants
- On recursion-free Horn clauses and Craig interpolation
- Complete instantiation-based interpolation
- Predicate diagrams for the verification of real-time systems
- Constraint solving for interpolation
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Verification Modulo theories
- Efficient generation of small interpolants in CNF
- Model checking duration calculus: a practical approach
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
- Verification and falsification of programs with loops using predicate abstraction
- View-augmented abstractions
- Refinement of Trace Abstraction
- Interpolation and Model Checking
- LCTD: test-guided proofs for C programs on LLVM
- Predicate Abstraction for Program Verification
- SAT-Based Model Checking
- Abstraction refinement with Craig interpolation and symbolic pushdown systems
- Refining abstract interpretations
- Parallel program analysis via range splitting
- Distributed and Predictable Software Model Checking
- Probabilistic CEGAR
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Specifying graph languages with type graphs
- Abstractions of uniform proofs
- Learning inductive invariants by sampling from frequency distributions
- On interpolation in automated theorem proving
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Abstraction, Axiomatization and Rigor: Pasch and Hilbert
- Predicate Abstraction in Program Verification: Survey and Current Trends
- Infinite-state invariant checking with IC3 and predicate abstraction
- An interpolating theorem prover
- Abstraction and Abstraction Refinement
- Computer Aided Verification
- On Interpolation in Decision Procedures
- A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
- 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)
