Efficient Interpolation for the Theory of Arrays. - Jochen Hoenicke; Tanja Schindler (SMT, 2017)

Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution). - Daniel Dietsch; Marius Greitschus; Matthias Heizmann; Jochen Hoenicke; Alexander Nutz; Andreas Podelski; Christian Schilling 001; Tanja Schindler (TACAS (2), 2018)

Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). - Matthias Heizmann; Yu-Fang Chen 001; Daniel Dietsch; Marius Greitschus; Jochen Hoenicke; Yong Li 031; Alexander Nutz; Betim Musa; Christian Schilling 001; Tanja Schindler; Andreas Podelski (TACAS (2), 2018)

Selfless Interpolation for Infinite-State Model Checking. - Tanja Schindler; Dejan Jovanovic (VMCAI, 2018)

Solving and Interpolating Constant Arrays Based on Weak Equivalences. - Jochen Hoenicke; Tanja Schindler (VMCAI, 2019)

Interpolation and the Array Property Fragment. - Jochen Hoenicke; Tanja Schindler (CoRR, 2019)

Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality. - Elisabeth Henkel; Jochen Hoenicke; Tanja Schindler (SMT, 2021)

Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching. - Jochen Hoenicke; Tanja Schindler (VMCAI, 2021)

A Simple Proof Format for SMT. - Jochen Hoenicke; Tanja Schindler (SMT, 2022)

SMT solving, interpolation, and quantifiers. - Tanja Schindler (2022)

SMT-Solving, Interpolation und Quantoren. - Tanja Schindler (Ausgezeichnete Informatikdissertationen, 2022)

Ultimate Automizer (SV-COMP 2022 - Modified). - Matthias Heizmann; Max Barth; Daniel Dietsch; Leonard Fichtner; Jochen Hoenicke; Dominik Klumpp; Mehdi Naouar; Tanja Schindler; Frank Schüssele; Andreas Podelski (Zenodo, 2022)

Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT. - Elisabeth Henkel; Jochen Hoenicke; Tanja Schindler (CADE, 2023)

Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution). - Matthias Heizmann; Max Barth; Daniel Dietsch; Leonard Fichtner; Jochen Hoenicke; Dominik Klumpp; Mehdi Naouar; Tanja Schindler; Frank Schüssele; Andreas Podelski (TACAS (2), 2023)

Pseudo-Boolean Proof Logging for Optimal Classical Planning. - Simon Dold 001; Malte Helmert; Jakob Nordström; Gabriele Röger; Tanja Schindler (CoRR, 2025)