Name: Shaukat Ali
Affiliation: Simula Research Laboratory, Norway
Homepage: https://www.simula.no/people/shaukat

Bio:
Shaukat Ali is a Chief Research Scientist, Research Professor, and Head of the Department at Simula Research Laboratory, Norway. He is also an adjunct associate professor at Oslo Metropolitan University, Oslo, Norway. He focuses on devising novel methods for verifying and validating classical and quantum software systems. He has led many national and European projects related to testing, search-based software engineering, model-based system engineering, and quantum software engineering.

Name: Mahsa Varshosaz
Affiliation: IT University of Copenhagen, Denmark
Homepage: http://mahsavarshosaz.net/

Bio:
Mahsa Varshosaz is an assistant professor at IT University of Copenhagen. Her research is focused on quality assurance and safety of software systems. She is interested in both theoretical and practical aspects of modeling, testing, and verification of systems and the challenges in the application of such techniques in different domains. She has experience developing and applying modeling and model-based testing techniques for families of software systems. More recently, she works on testing underwater robotic systems in the REMARO ITN where she is vice-coordinator for the project.

Testing Cyber-Physical Systems: Synergizing Model and AI-based Approaches.
One of the systematic and automated approaches for testing Cyber-Physical Systems (CPSs) is through Model-Based Testing (MBT). This method involves creating an abstract representation of a CPS, which is then utilized by an automated testing tool to generate executable test cases. This process enables the CPS to be thoroughly and systematically tested. Given the complexity of real-world CPS, there is a further need to optimize testing with Artificial Intelligence (AI)-based approaches such as genetic algorithms. This tutorial will have two main parts. The first part will cover the basics of MBT and relevant AI-based approaches for test optimization. The second part will present how these techniques are used to test real-world CPSs, such as communication systems, automated warehouses, and robots.

Name: Ina Schaefer
Affiliation: Karlsruhe IT, Germany
Homepage: https://tva.kastel.kit.edu/english/team_schaefer.php

Bio:
Ina Schaefer is a full professor at the Karlsruhe Institute of Technology (KIT), Germany, since April 2022 and heads the research group "Test, Validation, and Analysis of Software-Intensive Systems (TVA)" at the Institute for Information Security and Reliability (KASTEL). Previously, she was a professor of Software Engineering and Automotive Informatics at the Technical University of Braunschweig, Germany, for about ten years. She completed her doctorate in October 2008 at the TU Kaiserslautern, Germany. Her postdoctoral period took her to Chalmers University of Technology in Gothenburg, Sweden, from September 2009 to October 2010. The focus of her research is the integration of formal methods into software development, so that software can become better than it currently is. She is particularly interested in aspects of scalability, modularity, and reusability. Applications for this work can be found in a variety of systems, including automotive, aviation, and automation.

Name: Maximilian Kodetzki
Affiliation: Karlsruhe IT, Germany
Homepage: https://tva.kastel.kit.edu/english/team_kodetzki.php

Bio:
Maximilian Kodetzki is a PhD student at Karlsruhe Institute of Technology (KIT), Germany, since July 2023. He is part of the research group "Test, Validation and Analysis of Software-Intensive Systems (TVA)" at the Institute for Information Security and Reliability (KASTEL). The focus of his research is the functional correctness of software product lines using formal methods. Especially for safety-critical systems, the correctness is essential. Guaranteeing this correctness for product lines is difficult due to the implemented variability and the exponential explosion of software products.

The Correctness-by-Construction Approach to Programming Using CorC.
The Correctness-by-Construction tutorial focuses on an incremental programming approach to develop provable correct software. The purpose of the tutorial is to influence the participants' approaches to algorithm development using a technique that balances between formal methods and a "hack into correctness" style. The tutorial features a step-by-step introduction to how to derive functional correct algorithms using small refinement rules. Using carefully selected examples, the methodology can be applied by the participants in the tool WebCorC. Further, the tutorial showcases practical demonstrations of how non-trivial algorithms can be successfully derived. The tutorial bridges two extreme software development methodologies. On one side, approaches that are so formal that they even scare off experienced theoretical computer scientists. On the other side, there are some who believe that formality is a waste of time and develop software based on intuition and gut feelings. Our aim is to guide the participants towards a middle ground, where software development is both rigorous and pragmatic, but results in developing correct software.

Name: Einar Broch Johnsen
Affiliation: University of Oslo, Norway
Homepage: https://ebjohnsen.org/

Bio:
Einar Broch Johnsen is a professor at the Department of Informatics, University of Oslo. He is active in formal methods for distributed and concurrent systems, including object-oriented and actor languages, manycore computing, cloud computing and digital twins. He is one of the main developers of the ABS modeling language. He has been prominently involved in many national and European research projects; in particular, he was the strategy director of Sirius, a center for research-driven innovation on scalable data access, he was the coordinator of the EU FP7 project Envisage (2013-2016) on formal methods for cloud computing and the scientific coordinator of the EU H2020 project HyVar (2015-2018) on hybrid variability systems. Einar Broch Johnsen is member of IFIP WG2.2 “Formal Description of Programming Concepts”. He was board member of Sintef ICT (2009-2015). He is currently member of the Scientific Council of the dScience centre at University of Oslo, board member of Formal Methods Europe, editorial board member of the journals Formal Aspects of Computing and Journal of Logical and Algebraic Methods in Programming, and steering committee member of various conference series.

The Semantically Lifted Digital Twin.
Digital twin applications use digital artefacts to twin physical systems. The purpose is to continuously mirror the structure and behavior of the physical system, such that users can analyse the physical system by means of the digital twin for e.g., to give support for decision making, for systematic reconfiguration, etc. In this tutorial, we discuss what is a digital twin, and how it can be built in a framework that integrates semantic technology and simulation units. We also discuss how a digital twin can systematically reconfigure over time to mirror a changing physical system.

Name: Maurice H. ter Beek
Affiliation: Istituto di Scienza e Tecnologie dell'Informazione, Italy
Homepage: http://fmt.isti.cnr.it/~mtbeek/

Bio:
Maurice ter Beek is senior researcher at ISTI-CNR (Pisa, Italy) and head of the Formal Methods and Tools lab. He obtained his Ph.D. at Leiden University (The Netherlands). He has authored over 150 peer-reviewed papers, edited over 30 proceedings and special issues of journals, and serves on the editorial boards of the journals Formal Aspects of Computing: Applicable Formal Methods, International Journal on Software Tools for Technology Transfer, Journal of Logical and Algebraic Methods in Programming, PeerJ Computer Science, Science of Computer Programming, and ERCIM News. He works on formal methods and model-checking tools for the specification and verification of safety-critical software systems, focusing in particular on applications in service computing, software product line engineering and railway systems. He is member of the Steering Committees of the COORDINATION, FMICS (currently chair), iFM, SPLC and VaMoS conference series, and regular PC member of the ABZ, COORDINATION, FM, FMICS, FormaliSE, iFM, SEFM, SPLC and VaMoS conference series, among others. He is a board member of Formal Methods Europe (FME).

Formal Methods and Tools for Software Product Lines.
In this tutorial, the participants are introduced to Software Product Lines (SPLs) and in particular the field of behavioral variability modeling and analysis. They are made familiar with Featured Transition Systems (FTSs), Modal Transition Systems (MTSs) with variability constraints, and family-based analysis of such models. After explaining ambiguities in FTSs, the participants are introduced to SAT solving, and they are shown how to use it for static analysis of FTSs to detect ambiguities. Finally, a toolchain built around the Variability Model Checker VMC is presented, and it demonstrates how to use VMC to perform an efficient kind of family-based model checking of deadlock-free FTSs and MTSs. It also demonstrates how to use the front-end tool FTS4VMC to detect and remove ambiguities in an FTS, and to transform the resulting FTS into an MTS to make it amenable for analysis with VMC.

Name: Martin Leucker
Affiliation:University of Lübeck, Germany
Homepage: https://www.isp.uni-luebeck.de/leucker

Bio:
Martin Leucker received the Ph.D. degree from RWTH Aachen University, Germany. He worked as a Postdoctoral Researcher with the University of Pennsylvania, USA; and Uppsala University, Sweden. He pursued his habilitation at TU München, Germany. He is currently a Professor with the University of Lübeck, Germany, heading the Institute of Software Engineering and Programming Languages. Moreover, he is the CEO of UniTransferKlinik Lübeck GmbH, which also focuses on regulatory affairs, especially for medical devices. He is the author of more than 130 peer-reviewed journal and conference articles ranging over software engineering, formal methods, and theoretical computer science. His research interests include software engineering; correct and reliable systems; and formal methods and theoretical computer science, both from a technical and a regulatory perspective.

Automata Learning with an Application to Learn and Verify Recurrent Neural Networks.
In this tutorial, the participants are introduced to Automata Learning with applications to Formal Methods. We introduce the concepts of both passive and active automata learning for learning regular languages. Moreover, we present extensions for learning in the presence of unknowns as well as learning timed and data automata. Finally, we present several potential applications in the setting of formal verification. In particular, we show the methods that can be applied to verify recurrent neural networks.