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]
If you feel like your paper should be listed here, feel free to contact us.