SMTInterpol: An Interpolating SMT Solver. - Jürgen Christ; Jochen Hoenicke; Alexander Nutz (SPIN, 2012)

Proof Tree Preserving Interpolation. - Jürgen Christ; Jochen Hoenicke; Alexander Nutz (TACAS, 2013)

Ultimate Automizer with SMTInterpol - (Competition Contribution). - Matthias Heizmann; Jürgen Christ; Daniel Dietsch; Evren Ermis; Jochen Hoenicke; Markus Lindenmann; Alexander Nutz; Christian Schilling 001; Andreas Podelski (TACAS, 2013)

Ultimate Kojak - (Competition Contribution). - Evren Ermis; Alexander Nutz; Daniel Dietsch; Jochen Hoenicke; Andreas Podelski (TACAS, 2014)

ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution). - Alexander Nutz; Daniel Dietsch; Mostafa Mahmoud Mohamed; Andreas Podelski (TACAS, 2015)

Craig vs. Newton in software model checking. - Daniel Dietsch; Matthias Heizmann; Betim Musa; Alexander Nutz; Andreas Podelski (ESEC/SIGSOFT FSE, 2017)

Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution). - Marius Greitschus; Daniel Dietsch; Matthias Heizmann; Alexander Nutz; Claus Schätzle; Christian Schilling 001; Frank Schüssele; Andreas Podelski (TACAS (2), 2017)

Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution). - Matthias Heizmann; Yu-Wen Chen; Daniel Dietsch; Marius Greitschus; Alexander Nutz; Betim Musa; Claus Schätzle; Christian Schilling 001; Frank Schüssele; Andreas Podelski (TACAS (2), 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)

The Map Equality Domain. - Daniel Dietsch; Matthias Heizmann; Jochen Hoenicke; Alexander Nutz; Andreas Podelski (VSTTE, 2018)

A Tree-Based Approach to Data Flow Proofs. - Jochen Hoenicke; Alexander Nutz; Andreas Podelski (VSTTE, 2018)

Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages. - Daniel Dietsch; Matthias Heizmann; Jochen Hoenicke; Alexander Nutz; Andreas Podelski (CoRR, 2019)

Ultimate TreeAutomizer (CHC-COMP Tool Description). - Daniel Dietsch; Matthias Heizmann; Jochen Hoenicke; Alexander Nutz; Andreas Podelski (HCVS/PERR@ETAPS, 2019)

Data flow in program verification. - Alexander Nutz (2019)

Ultimate Automizer SV-COMP 2020 Competition Contribution. - Matthias Heizmann; Max Barth; Daniel Dietsch; Jill Enke; Leonard Fichtner; Dominik Klumpp; Mehdi Naouar; Lars Nitzke; Alexander Nutz; Andreas Podelski; Elisabeth Schanno; Claus Schätzle (Zenodo, 2019)

Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. - Shuvendu K. Lahiri; Akash Lal; Sridhar Gopinath; Alexander Nutz; Vladimir Levin; Rahul Kumar 002; Nate Deisinger; Jakob Lichtenberg; Chetan Bansal (FMCAD, 2020)

Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions - (Competition Contribution). - Daniel Dietsch; Matthias Heizmann; Alexander Nutz; Claus Schätzle; Frank Schüssele (TACAS (2), 2020)

Separating Map Variables in a Logic-Based Intermediate Verification Language. - Daniel Dietsch; Matthias Heizmann; Jochen Hoenicke; Alexander Nutz; Andreas Podelski (NETYS, 2021)

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification. - Petra Hozzová; Jaroslav Bendík; Alexander Nutz; Yoav Rodeh (LPAR, 2023)