Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

DOI10.1007/978-3-031-38499-8_15MaRDI QIDQ6492748zbMATH OpenFDO

Authors Jochen Hoenicke, Tanja I. Schindler

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_15

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Abstraction Refinement for Quantified Array Assertions
• Abstractions from proofs
• An efficient and flexible approach to resolution proof reduction
• Automated Deduction – CADE-20
• Cell morphing: from array programs to array-free Horn clauses
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• First-order interpolation and interpolating proof systems
• Interpolation Properties and SAT-Based Model Checking
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Nested interpolants
• On interpolation in automated theorem proving
• On recursion-free Horn clauses and Craig interpolation
• Predicate abstraction and refinement for verifying multi-threaded programs
• Proof tree preserving tree interpolation
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Splitting proofs for interpolation
• Thread modularity at many levels: a pearl in compositional verification
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tools and Algorithms for the Construction and Analysis of Systems
• Tree Interpolation in Vampire
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492748)