Farkas-based tree interpolation

DOI10.1007/978-3-030-65474-0_16zbMath1474.68321OpenAlexW3120197190MaRDI QIDQ2233543

Grigory Fedyukovich, Sepideh Asadi, Natasha Sharygina, Antti E. J. Hyvärinen, Martin Blicha

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-65474-0_16

zbMATH Keywords

Craig interpolationsymbolic model checkingSMT solvingLRA interpolation systemstree interpolation property

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Interpolation, preservation, definability (03C40)

Related Items (1)

SMT-based verification of program changes through summary repair

Cites Work

• Proof tree preserving tree interpolation
• OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
• Tree Interpolation in Vampire
• Efficient generation of craig interpolants in satisfiability modulo theories
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Simplify: a theorem prover for program checking
• Interpolant Strength
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Interpolation Properties and SAT-Based Model Checking
• Nested interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• eVolCheck: Incremental Upgrade Checker for C
• Predicate abstraction and refinement for verifying multi-threaded programs
• Constraint Solving for Interpolation
• Computer Aided Verification
• Decomposing Farkas Interpolants

This page was built for publication: Farkas-based tree interpolation