We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Paper accepted at FSE 2026!

Publications of Max Barth

Articles in journal or book chapters
  1. Max Barth, Matthias Heizmann, and Jochen Hoenicke. A lazy and modular approach to int-blasting. Acta Informatica, 63(16), 2026. doi:10.1007/s00236-026-00529-y Link to this entry Funding: DFG-ConVeY, DFG-ReVeriX Publisher's Version PDF
    BibTeX Entry
    @article{intBlasting, author = {Max Barth and Matthias Heizmann and Jochen Hoenicke}, title = {A lazy and modular approach to int-blasting}, journal = {Acta Informatica}, volume = {63}, number = {16}, pages = {}, year = {2026}, doi = {10.1007/s00236-026-00529-y}, url = {}, pdf = {}, keyword = {}, annote = {}, artifact = {}, funding = {DFG-ConVeY, DFG-ReVeriX}, }

Articles in conference or workshop proceedings
  1. Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Körner, Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, and Andreas Podelski. Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution). In Proc. TACAS, LNCS 16506, pages 589-594, 2026. Springer. doi:10.1007/978-3-032-22749-2_37 Link to this entry Keyword(s): Ultimate Automizer, Software Model Checking Publisher's Version PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{UAutomizer-SVCOMP2026, author = {Manuel Bentele and Max Barth and Marcel Ebbinghaus and Jan K{\"{o}}rner and Daniel Dietsch and Matthias Heizmann and Dominik Klumpp and Frank Sch{\"{u}}ssele and Andreas Podelski}, title = {Ultimate Automizer with a One-Dimensional Memory Model - (Competition Contribution)}, booktitle = {Proc.\ {TACAS}}, pages = {589--594}, year = {2026}, series = {LNCS~16506}, publisher = {Springer}, doi = {10.1007/978-3-032-22749-2_37}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Model Checking}, annote = {}, artifact = {10.5281/zenodo.17735224}, funding = {}, }
  2. Max Barth, Daniel Dietsch, Matthias Heizmann, and Marie-Christine Jakobs. Ultimate TestGen: Combining Parallel Trace Abstraction and Symbolic Path Execution (Competition Contribution). In Proc. FASE, LNCS 16504, pages 492-496, 2026. Springer. doi:10.1007/978-3-032-22774-4_28 Link to this entry Keyword(s): Ultimate Automizer, Software Model Checking, Test-Case Generation Funding: DFG-ConVeY, DFG-ReVeriX Publisher's Version PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{UTestGen-TestComp2026, author = {Max Barth and Daniel Dietsch and Matthias Heizmann and Marie{-}Christine Jakobs}, title = {Ultimate TestGen: Combining Parallel Trace Abstraction and Symbolic Path Execution (Competition Contribution)}, booktitle = {Proc. {FASE}}, pages = {492--496}, year = {2026}, series = {LNCS~16504}, publisher = {Springer}, doi = {10.1007/978-3-032-22774-4_28}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Model Checking, Test-Case Generation}, annote = {}, artifact = {10.5281/zenodo.17792491}, funding = {DFG-ConVeY, DFG-ReVeriX}, }
  3. Max Barth, Daniel Dietsch, Matthias Heizmann, and Marie-Christine Jakobs. Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution). In Proc. TACAS, LNCS 16506, pages 595-599, 2026. Springer. doi:10.1007/978-3-032-22749-2_38 Link to this entry Keyword(s): Ultimate Automizer, Software Model Checking Funding: DFG-ConVeY, DFG-ReVeriX Publisher's Version PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{UParalizer, author = {Max Barth and Daniel Dietsch and Matthias Heizmann and Marie{-}Christine Jakobs}, title = {Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution)}, booktitle = {Proc. {TACAS}}, pages = {595--599}, year = {2026}, series = {LNCS~16506}, publisher = {Springer}, doi = {10.1007/978-3-032-22749-2_38}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Model Checking}, annote = {}, artifact = {10.5281/zenodo.17555227}, funding = {DFG-ConVeY, DFG-ReVeriX}, }
  4. Max Barth and Matthias Heizmann. A Bit-vector to Integer Translation with bv2nat and nat2bv. In International Workshop on Satisfiability Modulo Theories, CEUR Workshop Proceedings, pages 53-63, 2024. CEUR-WS.org. Link to this entry Funding: DFG-ConVeY PDF
    BibTeX Entry
    @inproceedings{DBLP:conf/smt/BarthH24, author = {Max Barth and Matthias Heizmann}, title = {A Bit-vector to Integer Translation with bv2nat and nat2bv}, booktitle = {International Workshop on Satisfiability Modulo Theories}, pages = {53--63}, year = {2024}, series = {{CEUR} Workshop Proceedings}, publisher = {CEUR-WS.org}, doi = {}, url = {}, pdf = {https://ceur-ws.org/Vol-3725/short9.pdf}, keyword = {}, annote = {}, artifact = {}, funding = {DFG-ConVeY}, }
  5. Max Barth and Marie-Christine Jakobs. Refining CEGAR-based Test-Case Generation with Feasibility Annotations. In Proc. TAP , LNCS , 2024. Springer. doi:10.1007/978-3-031-72044-4_3 Link to this entry Keyword(s): Ultimate Automizer, Software Testing Funding: DFG-ReVeriX Publisher's Version PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{UTestGen-Reuse, author = {Max Barth and Marie{-}Christine Jakobs}, title = {Refining CEGAR-based Test-Case Generation with Feasibility Annotations}, booktitle = {Proc.\ {TAP}}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, doi = {10.1007/978-3-031-72044-4_3}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Testing}, annote = {}, artifact = {10.5281/zenodo.11641893}, funding = {DFG-ReVeriX}, }
  6. Max Barth and Marie-Christine Jakobs. Test-Case Generation with Automata-based Software Model Checking. In Proc. SPIN , LNCS , 2024. Springer. doi:10.1007/978-3-031-66149-5_14 Link to this entry Keyword(s): Ultimate Automizer, Software Testing Publisher's Version PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{UTestGen, author = {Max Barth and Marie{-}Christine Jakobs}, title = {Test-Case Generation with Automata-based Software Model Checking}, booktitle = {Proc.\ {SPIN}}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, doi = {10.1007/978-3-031-66149-5_14}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Testing}, annote = {}, artifact = {10.5281/zenodo.10574234}, funding = {}, }
  7. Max Barth, Daniel Dietsch, Matthias Heizmann, and Marie-Christine Jakobs. Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution). In Proc. FASE , LNCS 14573, pages 326-330, 2024. Springer. doi:10.1007/978-3-031-57259-3_20 Link to this entry Keyword(s): Ultimate Automizer, Software Testing Publisher's Version PDF
    Artifact(s)
    BibTeX Entry
    @inproceedings{UTestGen-Competition, author = {Max Barth and Daniel Dietsch and Matthias Heizmann and Marie{-}Christine Jakobs}, title = {Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution)}, booktitle = {Proc.\ {FASE}}, pages = {326-330}, year = {2024}, series = {LNCS~14573}, publisher = {Springer}, doi = {10.1007/978-3-031-57259-3_20}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Testing}, annote = {}, artifact = {10.5281/zenodo.10071568}, funding = {}, }
  8. Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, and Andreas Podelski. Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution). In Proc. TACAS, LNCS 13994, pages 577-581, 2023. Springer. doi:10.1007/978-3-031-30820-8_39 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{UAutomizer-SVCOMP2023, author = {Matthias Heizmann and Max Barth and Daniel Dietsch and Leonard Fichtner and Jochen Hoenicke and Dominik Klumpp and Mehdi Naouar and Tanja Schindler and Frank Sch{\"{u}}ssele and Andreas Podelski}, title = {Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution)}, booktitle = {Proc. {TACAS}}, pages = {577--581}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_39}, url = {}, pdf = {}, keyword = {}, annote = {}, artifact = {}, funding = {}, }

Internal reports
  1. Max Barth and Marie-Christine Jakobs. Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement. Technical report 2509.13699, arXiv/CoRR, 2025. doi:10.48550/ARXIV.2509.13699 Link to this entry Keyword(s): Ultimate Automizer, Software Model Checking Publisher's Version PDF
    BibTeX Entry
    @techreport{ParallelTraceAbstraction-TechReport, author = {Max Barth and Marie{-}Christine Jakobs}, title = {Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement}, number = {2509.13699}, year = {2025}, doi = {10.48550/ARXIV.2509.13699}, url = {}, pdf = {}, keyword = {Ultimate Automizer, Software Model Checking}, annote = {}, artifact = {}, funding = {}, institution = {arXiv/CoRR}, }

Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Last modified: Fri May 15 01:05:03 2026 UTC