Software and Computational Systems Lab

Funding by DFG-ConVeY

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

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