Efficient generation of craig interpolants in satisfiability modulo theories
From MaRDI portal
Publication:2946624
DOI10.1145/1838552.1838559zbMath1351.68247arXiv0906.4492OpenAlexW2003690673WikidataQ62041234 ScholiaQ62041234MaRDI QIDQ2946624
Alberto Griggio, Alessandro Cimatti, Roberto Sebastiani
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0906.4492
Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Related Items
Infinite-state invariant checking with IC3 and predicate abstraction, Whale: An Interpolation-Based Algorithm for Inter-procedural Verification, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Interpolation systems for ground proofs in automated deduction: a survey, Craig Interpolation in the Presence of Non-linear Constraints, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, Satisfiability Modulo Theories, Optimization Modulo Theories with Linear Rational Costs, Verification Modulo theories, Local abstraction refinement for probabilistic timed programs, Farkas-based tree interpolation, Parallelizing SMT solving: lazy decomposition and conciliation, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, On recursion-free Horn clauses and Craig interpolation, \textsc{OptiMathSAT}: a tool for optimization modulo theories, On interpolation in automated theorem proving
