Publications about SMTInterpol

• Elisabeth Henkel, Jochen Hoenicke and Tanja Schindler. Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality. In SMT 2021. [pdf]
• Jochen Hoenicke and Tanja Schindler. Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching. In VMCAI 2021. [doi] [bib]
• Jochen Hoenicke and Tanja Schindler. Solving and Interpolating Constant Arrays Based on Weak Equivalences. In VMCAI 2019. [doi] [bib]
• Jochen Hoenicke and Tanja Schindler. Efficient Interpolation for the Theory of Arrays. In IJCAR 2018. [doi] [bib] Authors' version at arXiv.
• Jürgen Christ and Jochen Hoenicke. Proof Tree Preserving Tree Interpolation. In Journal of Automated Reasoning (57) 1. [doi] [bib]
• Jürgen Christ and Jochen Hoenicke. Cutting the Mix. In CAV 2015. [doi] [bib]
• Jürgen Christ and Jochen Hoenicke. Weakly Equivalent Arrays. In FroCos 2015. [doi] [bib]
• Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. Proof Tree Preserving Interpolation. In TACAS 2013. [pdf] [doi] [bib] Authors' version at arXiv.
• Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An Interpolating SMT Solver. In SPIN 2012. [pdf] [doi] [bib]
• Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol system description for the SMT-COMP 2012. [pdf]

Publications using SMTInterpol

• Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, Andreas Podelski. Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). In TACAS 2018. [doi] [bib]
• Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling, Tanja Schindler. Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution). In TACAS 2018. [doi] [bib]
• Evren Ermis, Jochen Hoenicke, and Andreas Podelski. Splitting via Interpolants. In VMCAI 2012. [pdf] [doi] [bib]
• Evren Ermis, Martin Schäf, and Thomas Wies. Error Invariants. In FM 2012. [pdf] [doi] [bib]