Matthias Heizmann

62 papers A* 5A 6B 7C 3Journal 15Unranked 24
YearRankTypeTitle / Venue / Authors
2026 J jnl
A lazy and modular approach to int-blasting.
Acta Informatica
Max Barth, Matthias Heizmann, Jochen Hoenicke
2026 — conf
Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution).
TACAS (2)
Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Körner, Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, Andreas Podelski
2026 — conf
Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution).
TACAS (2)
Max Barth, Daniel Dietsch, Matthias Heizmann, Marie-Christine Jakobs
2026 B conf
Ultimate TestGen: Combining Parallel Trace Abstraction and Symbolic Path Execution (Competition Contribution).
FASE
Max Barth, Daniel Dietsch, Matthias Heizmann, Marie-Christine Jakobs
2025 — conf
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts.
VMCAI (1)
Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schüssele, Michael Schwarz, Helmut Seidl, Sarah Tilscher, Vesal Vojdani
2025 J jnl
Correctness Witnesses with Function Contracts.
CoRR
Matthias Heizmann, Dominik Klumpp, Marian Lingsch Rosenfeld, Frank Schüssele
2024 — conf
A Bit-vector to Integer Translation with bv2nat and nat2bv.
SMT@CAV
Max Barth, Matthias Heizmann
2024 J jnl
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version).
CoRR
Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schüssele, Michael Schwarz, Helmut Seidl, Sarah Tilscher, Vesal Vojdani
2024 — conf
Petrification: Software Model Checking for Programs with Dynamic Thread Management.
VMCAI (2)
Matthias Heizmann, Dominik Klumpp, Lars Nitzke, Frank Schüssele
2024 — conf
Ultimate Automizer and the Abstraction of Bitwise Operations - (Competition Contribution).
TACAS (3)
Frank Schüssele, Manuel Bentele, Daniel Dietsch, Matthias Heizmann, Xinyu Jiang, Dominik Klumpp, Andreas Podelski
2024 B conf
Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution).
FASE
Max Barth, Daniel Dietsch, Matthias Heizmann, Marie-Christine Jakobs
2023 J jnl
Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version).
CoRR
Matthias Heizmann, Dominik Klumpp, Frank Schüssele, Lars Nitzke
2023 — conf
Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution).
TACAS (2)
Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, Andreas Podelski
2023 — conf
Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution).
TACAS (2)
Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, Andreas Podelski
2022 — conf
Ultimate GemCutter and the Axes of Generalization - (Competition Contribution).
TACAS (2)
Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, Andreas Podelski
2022 J jnl
Verification Witnesses.
ACM Trans. Softw. Eng. Methodol.
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Thomas Lemberger, Michael Tautschnig
2021 — conf
Separating Map Variables in a Logic-Based Intermediate Verification Language.
NETYS
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2021 B conf
Verification of Concurrent Programs Using Petri Net Unfoldings.
VMCAI
Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schätzle
2020 — ed.
Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT/HCVS@ETAPS 2020, Dublin, Ireland, 25-26th April 2020.
VPT/HCVS@ETAPS
Laurent Fribourg, Matthias Heizmann
2020 A* conf
The IBM z15 High Frequency Mainframe Branch Predictor Industrial Product.
ISCA
Narasimha Adiga, James Bonanno, Adam Collura, Matthias Heizmann, Brian R. Prasky, Anthony Saporito
2020 — conf
Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions - (Competition Contribution).
TACAS (2)
Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Frank Schüssele
2019 J jnl
Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages.
CoRR
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2019 — conf
Semantic Fault Localization and Suspiciousness Ranking.
TACAS (1)
Maria Christakis, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, Valentin Wüstholz
2019 J jnl
The SMT Competition 2015-2018.
J. Satisf. Boolean Model. Comput.
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
2019 — conf
Ultimate TreeAutomizer (CHC-COMP Tool Description).
HCVS/PERR@ETAPS
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2018 A* conf
Advanced automata-based algorithms for program termination checking.
PLDI
Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang
2018 — conf
Geometric Nontermination Arguments.
TACAS (2)
Jan Leike, Matthias Heizmann
2018 B conf
Incremental Verification Using Trace Abstraction.
SAS
Bat-Chen Rothenberg, Daniel Dietsch, Matthias Heizmann
2018 — conf
The Map Equality Domain.
VSTTE
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski
2018 — conf
Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2)
Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, Andreas Podelski
2018 — conf
Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution).
TACAS (2)
Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling, Tanja Schindler
2017 — conf
Craig vs. Newton in software model checking.
ESEC/SIGSOFT FSE
Daniel Dietsch, Matthias Heizmann, Betim Musa, Alexander Nutz, Andreas Podelski
2017 C conf
Exchanging Verification Witnesses between Verifiers.
Software Engineering
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann
2017 — conf
Minimization of Visibly Pushdown Automata Using Partial Max-SAT.
TACAS (1)
Matthias Heizmann, Christian Schilling, Daniel Tischner
2017 J jnl
Minimization of Visibly Pushdown Automata Using Partial Max-SAT.
CoRR
Matthias Heizmann, Christian Schilling, Daniel Tischner
2017 — conf
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution).
TACAS (2)
Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling, Frank Schüssele, Andreas Podelski
2017 — conf
Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution).
TACAS (2)
Marius Greitschus, Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, Andreas Podelski
2016 A conf
Complementing Semi-deterministic Büchi Automata.
TACAS
Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai
2016 — conf
Correctness witnesses: exchanging verification results between verifiers.
SIGSOFT FSE
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann
2016 J jnl
Geometric Nontermination Arguments.
CoRR
Jan Leike, Matthias Heizmann
2016 A conf
Ultimate Automizer with Two-track Proofs - (Competition Contribution).
TACAS
Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schätzle, Andreas Podelski
2016 C conf
Witness validation and stepwise testification across software verifiers.
Software Engineering
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Andreas Stahlbauer
2015 C conf
Automated Program Verification.
LATA
Azadeh Farzan, Matthias Heizmann, Jochen Hoenicke, Zachary Kincaid, Andreas Podelski
2015 — conf
Fairness Modulo Theory: A New Approach to LTL Software Model Checking.
CAV (1)
Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, Andreas Podelski
2015 J jnl
Ranking Templates for Linear Loops.
Log. Methods Comput. Sci.
Jan Leike, Matthias Heizmann
2015 — —
Traces, interpolants, and automata: a new approach to automatic software verification.
Matthias Heizmann
2015 A conf
Ultimate Automizer with Array Interpolation - (Competition Contribution).
TACAS
Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Andreas Podelski
2015 — conf
Witness validation and stepwise testification across software verifiers.
ESEC/SIGSOFT FSE
Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Andreas Stahlbauer
2014 J jnl
Geometric Series as Nontermination Arguments for Linear Lasso Programs.
CoRR
Jan Leike, Matthias Heizmann
2014 J jnl
Linear Ranking for Linear Lasso Programs.
CoRR
Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski
2014 A conf
Ranking Templates for Linear Loops.
TACAS
Jan Leike, Matthias Heizmann
2014 J jnl
Ranking Templates for Linear Loops.
CoRR
Jan Leike, Matthias Heizmann
2014 A* conf
Termination Analysis by Learning Terminating Programs.
CAV
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2014 J jnl
Termination Analysis by Learning Terminating Programs.
CoRR
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2014 A conf
Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution).
TACAS
Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski
2013 B conf
Linear Ranking for Linear Lasso Programs.
ATVA
Matthias Heizmann, Jochen Hoenicke, Jan Leike, Andreas Podelski
2013 A* conf
Software Model Checking for People Who Love Automata.
CAV
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2013 A conf
Ultimate Automizer with SMTInterpol - (Competition Contribution).
TACAS
Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski
2010 A* conf
Nested interpolants.
POPL
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
2010 B conf
Size-Change Termination and Transition Invariants.
SAS
Matthias Heizmann, Neil D. Jones, Andreas Podelski
2009 J jnl
Functional verification of the IBM System z10 processor chipset.
IBM J. Res. Dev.
Christopher A. Krygowski, Dean G. Bair, Rebecca M. Gott, Mark H. Decker, A. V. Giri, Christian Habermann, Matthias Heizmann, Stefan Letz, William J. Lewis, Steven M. Licker, H. Mallar, Edward C. McCain, Wolfgang Roesner, Nafiul Siddique, A. E. Seigler, Brian W. Thompto, Kai Weber, Ralf Winkelmann
2009 B conf
Refinement of Trace Abstraction.
SAS
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski