Software and Computational Systems Lab

Publications about Ultimate Automizer

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 Keyword(s): Ultimate Automizer, Software Model Checking Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.17735224
   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 Keyword(s): Ultimate Automizer, Software Model Checking, Test-Case Generation Funding: DFG-ConVeY, DFG-ReVeriX Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.17792491
   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 Keyword(s): Ultimate Automizer, Software Model Checking Funding: DFG-ConVeY, DFG-ReVeriX Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.17555227
   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 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 Keyword(s): Ultimate Automizer, Software Testing Funding: DFG-ReVeriX Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.11641893
   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}, }
5. 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 Keyword(s): Ultimate Automizer, Software Testing Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.10574234
   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 = {}, }
6. 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 Keyword(s): Ultimate Automizer, Software Testing Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.10071568
   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 = {}, }

7. 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 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}, }