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

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