Bernhard K. Aichernig

As part of the ongoing effort in the automotive domain to achieve automated driving, advanced driver assistance systems (ADAS) are designed for increasingly complex driving tasks. This includes safety-critical features such as automated lane-keeping and emergency braking. Consequently, validation and verification of ADAS are highly important. However, with the growing complexity of the automated driving tasks, the corresponding ADAS also increase in complexity, which makes validation and verification more costly. Hence, automation is needed. In this work, the domain of ADAS serves as a case study for learning-based testing (LBT). In particular, we apply active automata learning to infer formal behavioral models of ADAS during testing. This entails several challenges since such systems feature a mixture of continuous and discrete behavior as well as domain constraints. The setting exhibits a large search space with only a small portion of valid test cases. We exemplify how the right abstractions implemented through mappers can be used to deal with these challenges. Finally, we demonstrate the use of two different automata learning approaches in learning-based testing of an adaptive cruise controller and show that they are able to generate critical test cases.

This is an introduction to the proceedings for the track ‘AI Assisted Programming’ (AIAP), organized at the fourth instance of the AISoLA conference during the period October 27–31, 2026. AISoLA as a whole aims to study opportunities and risks of late advances of AI. The motivation behind the AIAP track in particular is the emerging use of large language models for the construction and analysis of software artifacts. An overview of the track presentations is provided.

In this work, we present an industrial case study of deadlock avoidance in the context of automated warehouse logistics. In particular, we consider systems of Automated Guided Vehicles (AGVs) in which semi-autonomous robots move inside a facility along a predefined set of paths. The paper introduces a novel formalization of AGV systems that models the physical setup of the AGV system more accurately compared to previous approaches. In particular, our modeling approach captures movement restrictions due to physical proximity of vehicles regardless of the logical connectivity of the guide path network. The paper provides and compares three different encodings of such models as transition systems, which enable symbolic analysis of the system via Binary Decision Diagrams (BDDs). Based on these encodings we perform deadlock avoidance for warehouse layouts of both synthetic and real-world origin.

Active automata learning enables model-based testing and verification of black-box systems by automatically constructing models from observations via interactions with the system. As interactions are usually expensive, active algorithms attempt to perform as few interactions as possible to learn a given system. However, many such algorithms struggle when confronted with noise, such as message loss, when learning otherwise deterministic systems. We investigate and adapt different algorithms to learn deterministic automata in a noisy setting. One of these is a novel active algorithm based on our previous passive Partial Max-SAT algorithm. In our analysis, we demonstrate techniques to lower the required number of interactions and order the evaluated algorithms accordingly. Finally, we show that the necessary interactions can be further reduced when leaving the classical active learning framework.

With the servitization of business, understanding how users experience services becomes a crucial success factor for companies. Therefore, there is a need to include feedback from user experiences in the software engineering process. Behavioral models of user journeys, describing how users experience their interaction with a service, can provide insights and potentially improve services. In this paper, we investigate techniques that allow the automatic generation of behavioral models from user interactions with a service, recorded in an event log. We first compare two established techniques that generate behavioral models from a given event log: automata learning and process mining. Afterward, we present a novel, hybrid method that combines both automata learning and process mining methods to overcome their limitations. For the existing techniques, we present methods to learn models of user journeys and evaluate the accuracy of the resulting models. We then compare these techniques with our novel method for the automatic extraction of user journey models from the event logs of digital services. We assess the practical applicability of all techniques by evaluating real-world applications. Our results show that process mining techniques rely on expert knowledge, while automata learning techniques depend on the distribution of events in the given event log. We further show that the proposed hybrid technique combines the strengths of both process mining and automata learning, automatically selecting the best method and parameter settings for a given event log to learn very accurate models.

This is an introduction to the track ‘AI Assisted Programming’ (AIAP), organized at the third instance of the AISoLA conference during the period November 1–5, 2025. AISoLA as a whole aims to study opportunities and risks of late advances of AI. The motivation behind the AIAP track in particular, which also takes place the third time, is the emerging use of large language models for the construction and analysis of software artifacts. An overview of the track presentations is provided.

AALpy is a well-established open-source automata learning library written in Python with a focus on active learning of systems with IO behavior. It provides a wide range of state-of-the-art algorithms for different automaton types ranging from fully deterministic to probabilistic automata. In this work, we present the recent addition of a generalized implementation of an important method from the domain of passive automata learning: state-merging in the red-blue framework. Using a common internal representation for different automaton types allows for a general and highly configurable implementation of the red-blue framework. We describe how to define and execute state-merging algorithms using AALpy, which reduces the implementation effort for state-merging algorithms mainly to the definition of compatibility criteria and scoring. This aids the implementation of both existing and novel algorithms. In particular, defining some existing state-merging algorithms from the literature with AALpy only takes a few lines of code.