Software and Computational Systems Lab

Publications of year 2026

1. Franco Barbanera and Rolf Hennicker. Safe Orchestrated Multicomposition of Systems of Communicating Finite State Machines. Journal of Logical and Algebraic Methods in Programming:101109, 2026. doi:10.1016/j.jlamp.2026.101109 Publisher's Version
   Abstract

   The Participants-as-Interfaces (PaI) approach to system composition suggests that participants in a system can be considered interfaces to the outside world. Given a set of systems, one participant per system is chosen to play the role of an interface. When systems are composed, these interface participants are replaced by gateways that communicate with each other by forwarding messages. The PaI approach for systems of asynchronously communicating finite state machines (CFSMs) has been exploited in the literature for binary composition where the forwarding policy is necessarily unique. In this paper we consider the case of multiple system composition and extend preliminary work to the case where interactions among gateways can be mediated by additional orchestrating participants that comply with a given connection model. We represent the interactions among gateways as CFSM systems (called orchestrated connection policies) and prove that a number of relevant communication properties (e.g. deadlock-freedom, reception-error-freedom) are preserved by orchestrated PaI multicomposition, provided that the orchestrated connection policy used also satisfies the communication property in question.
   BibTeX Entry

   @article{HennickerJLAP26, author = {Franco Barbanera and Rolf Hennicker}, title = {Safe Orchestrated Multicomposition of Systems of Communicating Finite State Machines}, journal = {Journal of Logical and Algebraic Methods in Programming}, pages = {101109}, year = {2026}, doi = {10.1016/j.jlamp.2026.101109}, abstract = {The Participants-as-Interfaces (PaI) approach to system composition suggests that participants in a system can be considered interfaces to the outside world. Given a set of systems, one participant per system is chosen to play the role of an interface. When systems are composed, these interface participants are replaced by gateways that communicate with each other by forwarding messages. The PaI approach for systems of asynchronously communicating finite state machines (CFSMs) has been exploited in the literature for binary composition where the forwarding policy is necessarily unique. In this paper we consider the case of multiple system composition and extend preliminary work to the case where interactions among gateways can be mediated by additional orchestrating participants that comply with a given connection model. We represent the interactions among gateways as CFSM systems (called orchestrated connection policies) and prove that a number of relevant communication properties (e.g. deadlock-freedom, reception-error-freedom) are preserved by orchestrated PaI multicomposition, provided that the orchestrated connection policy used also satisfies the communication property in question.}, issn = {2352-2208}, }

2. D. Beyer, T. Lemberger, and H. Wachowitz. Testing in Formal Verification via Witness Generation (Empirical Evaluation). In Proceedings of the 29th International Conference on Fundamental Approaches to Software Engineering (FASE 2026, Turin, Italy, April 11-16), LNCS 16504, 2026. Springer. Keyword(s): Software Model Checking, Software Testing Funding: DFG-CONVEY, DFG-COOP PDF
   Artifact(s)

   1. doi:10.5281/zenodo.18190957
   Abstract

   Despite potential synergies, the communities surrounding formal software verifiers and automatic test generators have developed different formats to describe a path to an error. Test generators export a test case whose execution makes the error observable, while verifiers produce a violation witness, an abstract description of the error path. Previous work transformed violation witnesses into test cases and evaluated their effectiveness, and other work found that test generators are more effective in bug finding than formal verifiers. While there are hybrid approaches to formal verification that utilize testing, there is no empirical evaluation of the usefulness of the off-the-shelf use of test generators in formal verification. We change that by transforming test cases to violation witnesses. This allows the use of test generators for finding counterexamples in verification scenarios like the Competition on Software Verification (SV-COMP), both directly and as parts of bigger verification systems. In a large empirical evaluation we examine the potential improvements this use of test generators can add to formal verifiers.
   BibTeX Entry

   @inproceedings{FASE26a, author = {D.~Beyer and T.~Lemberger and H.~Wachowitz}, title = {Testing in Formal Verification via Witness Generation (Empirical Evaluation)}, booktitle = {Proceedings of the 29th International Conference on Fundamental Approaches to Software Engineering (FASE~2026, Turin, Italy, April 11-16)}, pages = {}, year = {2026}, series = {LNCS~16504}, publisher = {Springer}, doi = {}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2026-FASE.Testing_in_Formal_Verification_via_Witness_Generation.pdf}, abstract = {Despite potential synergies, the communities surrounding formal software verifiers and automatic test generators have developed different formats to describe a path to an error. Test generators export a test case whose execution makes the error observable, while verifiers produce a violation witness, an abstract description of the error path. Previous work transformed violation witnesses into test cases and evaluated their effectiveness, and other work found that test generators are more effective in bug finding than formal verifiers. While there are hybrid approaches to formal verification that utilize testing, there is no empirical evaluation of the usefulness of the off-the-shelf use of test generators in formal verification. We change that by transforming test cases to violation witnesses. This allows the use of test generators for finding counterexamples in verification scenarios like the Competition on Software Verification (SV-COMP), both directly and as parts of bigger verification systems. In a large empirical evaluation we examine the potential improvements this use of test generators can add to formal verifiers.}, keyword = {Software Model Checking, Software Testing}, artifact = {10.5281/zenodo.18190957}, funding = {DFG-CONVEY, DFG-COOP}, }
3. D. Beyer. Find, Use, and Conserve Tools for Formal Methods. In Proc. Festschrift Podelski 65th Birthday, LNCS 14765, pages 75-91, 2026. Springer. doi:10.1007/978-3-032-13711-1_5 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{Podelski65, author = {D.~Beyer}, title = {Find, Use, and Conserve Tools for Formal Methods}, booktitle = {Proc. Festschrift Podelski 65th Birthday}, pages = {75-91}, year = {2026}, series = {LNCS~14765}, publisher = {Springer}, doi = {10.1007/978-3-032-13711-1_5}, }
4. Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee, and Thomas Lemberger. A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module. In Proceedings of the 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026, Turin, Italy, April 11-16), LNCS, 2026. Springer. Keyword(s): Software Model Checking, Software Testing, Firmware verification Funding: DFG-CONVEY, DFG-BRIDGE, Intel Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.18371342
   Abstract

   Firmware underpins system security but remains challenging to verify due to hardware dependency, specialized coding idioms, and limited open-source examples. Manual verification approaches, while common in industry, are labor-intensive and difficult to scale. This paper presents a detailed case study on applying automatic formal methods for software to a security-critical firmware component in Intel Trust Domain Extensions (TDX), known as TDX Module. In this study, we employ six state-of-the-art C-program analyzers on the production TDX Module firmware, leveraging techniques ranging from bounded model checking and symbolic execution to abstract interpretation. Our empirical evaluation identifies obstacles unique to firmware, highlights harness-design decisions essential for verifying industry-scale code bases, and demonstrates opportunities in advanced slicing for more scalable verification. Although the case study focuses on TDX Module, the findings are broadly applicable to large-scale, low-level programs and have already influenced the software-verification community, such as standardizing nondeterministic object initialization. All verification tasks and proof harnesses are publicly released to foster reproducible research and future tool development.
   BibTeX Entry

   @inproceedings{TACAS26a, author = {Dirk Beyer and Po-Chun Chien and Bo-Yuan Huang and Nian-Ze Lee and Thomas Lemberger}, title = {{A} Case Study in Firmware Verification: {Applying} Formal Methods to {Intel TDX Module}}, booktitle = {Proceedings of the 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2026, Turin, Italy, April 11-16)}, pages = {}, year = {2026}, series = {LNCS}, publisher = {Springer}, doi = {}, url = {https://www.sosy-lab.org/research/tdx-module-firmware-verification/}, abstract = {Firmware underpins system security but remains challenging to verify due to hardware dependency, specialized coding idioms, and limited open-source examples. Manual verification approaches, while common in industry, are labor-intensive and difficult to scale. This paper presents a detailed case study on applying automatic formal methods for software to a security-critical firmware component in Intel Trust Domain Extensions (TDX), known as TDX Module. In this study, we employ six state-of-the-art C-program analyzers on the production TDX Module firmware, leveraging techniques ranging from bounded model checking and symbolic execution to abstract interpretation. Our empirical evaluation identifies obstacles unique to firmware, highlights harness-design decisions essential for verifying industry-scale code bases, and demonstrates opportunities in advanced slicing for more scalable verification. Although the case study focuses on TDX Module, the findings are broadly applicable to large-scale, low-level programs and have already influenced the software-verification community, such as standardizing nondeterministic object initialization. All verification tasks and proof harnesses are publicly released to foster reproducible research and future tool development.}, keyword = {Software Model Checking, Software Testing, Firmware verification}, annote = {This article has been selected as an "<a href="https://etaps.org/2026/programme/">ETAPS Distinguished Paper</a>." A preprint is available upon request and an <a href="https://www.sosy-lab.org/research/tdx-module-firmware-verification/tacas26-appendix.pdf">appendix</a> to this article is available on our supplementary webpage.}, artifact = {10.5281/zenodo.18371342}, funding = {DFG-CONVEY, DFG-BRIDGE, Intel}, }
   Additional Infos

   This article has been selected as an "ETAPS Distinguished Paper." A preprint is available upon request and an appendix to this article is available on our supplementary webpage.
5. Áron Ricardo Perez-Lopez, Po-Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan, and Clark Barrett. Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness. In Proceedings of the 27th International Symposium on Formal Methods (FM 2026, Tokyo, Japan, May 18-22), LNCS, 2026. Springer. Keyword(s): Btor2, SMT Funding: DFG-CONVEY, DFG-BRIDGE Supplement
   BibTeX Entry

   @inproceedings{Pono-FM26, author = {Áron Ricardo Perez-Lopez and Po-Chun Chien and Florian Lonsing and Samantha Archer and Ahmed Irfan and Clark Barrett}, title = {{Pono} 2.0: {A} Versatile {SMT}-Based Model Checker for Safety and Liveness}, booktitle = {Proceedings of the 27th International Symposium on Formal Methods (FM~2026, Tokyo, Japan, May 18-22)}, pages = {}, year = {2026}, series = {LNCS}, publisher = {Springer}, doi = {}, url = {https://github.com/stanford-centaur/pono}, pdf = {}, presentation = {}, abstract = {}, keyword = {Btor2, SMT}, artifact = {}, funding = {DFG-CONVEY, DFG-BRIDGE}, }
6. T. Lemberger and H. Wachowitz. AFL-TC: Transforming Fuzzer Test Inputs for Test-Comp (Competition Contribution). In Proceedings of the 29th International Conference on Fundamental Approaches to Software Engineering (FASE 2026, Turin, Italy, April 11-16), LNCS 16504, 2026. Springer. Keyword(s): Software Testing, Fuzzing Funding: DFG-CONVEY, DFG-COOP PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.18060896
   Abstract

   AFL-TC is a tool chain that integrates AFL++ into the environment of Test-Comp. Coverage-guided greybox fuzzers like AFL++ produce raw binary data that is given to programs as input on stdin, without any knowledge of how this data is interpreted. In contrast to that, Test-Comp requires structured XML descriptions of test cases that list a sequence of individual input values, which are read whenever the program calls an input function. Previous adaptations of fuzzers used tool-specific modifications for Test-Comp. Now, AFL-TC demonstrates a flexible solution that decouples the test generation from the Test-Comp format: AFL-TC first runs AFL++ (or any other tester that produces binary input for stdin), then replays each input with a test harness that (a) records how the test input is interpreted by the program and (b) outputs the recording as corresponding XML elements. To provide test cases early, AFL-TC employs a monitor that triggers a transformation whenever new test files are discovered. AFL-TC participated in both Test-Comp categories Cover-Error and Cover-Branches. It placed 6th overall, 4th among active participants, and best in the sub-category C.coverage-branches.Arrays
   BibTeX Entry

   @inproceedings{FASE26b, author = {T.~Lemberger and H.~Wachowitz}, title = {{AFL-TC}: Transforming Fuzzer Test Inputs for {Test-Comp} (Competition Contribution)}, booktitle = {Proceedings of the 29th International Conference on Fundamental Approaches to Software Engineering (FASE~2026, Turin, Italy, April 11-16)}, pages = {}, year = {2026}, series = {LNCS~16504}, publisher = {Springer}, doi = {}, url = {https://gitlab.com/sosy-lab/software/test-to-witness}, pdf = {https://www.sosy-lab.org/research/pub/2026-FASE.AFL-TC_Transforming_Fuzzer_Test_Inputs_for_Test-Comp.pdf}, abstract = {AFL-TC is a tool chain that integrates AFL++ into the environment of Test-Comp. Coverage-guided greybox fuzzers like AFL++ produce raw binary data that is given to programs as input on stdin, without any knowledge of how this data is interpreted. In contrast to that, Test-Comp requires structured XML descriptions of test cases that list a sequence of individual input values, which are read whenever the program calls an input function. Previous adaptations of fuzzers used tool-specific modifications for Test-Comp. Now, AFL-TC demonstrates a flexible solution that decouples the test generation from the Test-Comp format: AFL-TC first runs AFL++ (or any other tester that produces binary input for stdin), then replays each input with a test harness that (a) records how the test input is interpreted by the program and (b) outputs the recording as corresponding XML elements. To provide test cases early, AFL-TC employs a monitor that triggers a transformation whenever new test files are discovered. AFL-TC participated in both Test-Comp categories Cover-Error and Cover-Branches. It placed 6th overall, 4th among active participants, and best in the sub-category C.coverage-branches.Arrays}, keyword = {Software Testing, Fuzzing}, artifact = {10.5281/zenodo.18060896}, funding = {DFG-CONVEY, DFG-COOP}, }

7. Yuan Cui. Value Analysis with Initial Precision from YML Correctness Witness. Master's Thesis, LMU Munich, Software Systems Lab, 2026.
   BibTeX Entry

   @misc{WitnessReuseValueAnalysis, author = {Yuan Cui}, title = {Value Analysis with Initial Precision from YML Correctness Witness}, year = {2026}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
8. Yuemiao Xiang. Parallel Test-Case Generation via Test-Goal Splitting. Master's Thesis, LMU Munich, Software Systems Lab, 2026.
   BibTeX Entry

   @misc{ParallelTestingGoalSplit, author = {Yuemiao Xiang}, title = {Parallel Test-Case Generation via Test-Goal Splitting}, year = {2026}, field = {Computer Science}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }