Tree Interpolation in Vampire

DOI10.1007/978-3-642-45221-5_13MaRDI QIDQ2870125zbMATH OpenOpenAlexFDO

Authors Régis Blanc, Ashutosh Gupta, Laura Kovács, Bernhard Kragl

Publication date 17 January 2014

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://infoscience.epfl.ch/record/192948/files/LPAR13_Blanc.pdf

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40)

Recommendations

• Farkas-based tree interpolation
• Interpolation and symbol elimination in Vampire
• scientific article; zbMATH DE number 2127736
• scientific article; zbMATH DE number 1903379
• Open locating-dominating interpolation for trees
• Proof tree preserving tree interpolation
• scientific article; zbMATH DE number 5606397
• Vectorization of tree traversals
• Trees at an interface

Cited in

(6)

• The anatomy of vampire. Implementing bottom-up procedures with code trees
• Farkas-based tree interpolation
• Proof tree preserving tree interpolation
• Interpolation and symbol elimination in Vampire
• SMT-based verification of program changes through summary repair
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

Describes a project that uses

Uses Software

• VAMPIRE
• z3

This page was built for publication: Tree Interpolation in Vampire

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