Speakers

This course introduces the fundamentals of automata learning and its close connection to black-box testing, using the open-source tool AALpy (https://github.com/DES-Lab/AALpy). The presented learning-based testing approach combines the active inference of finite-state models with systematic model-based test-case generation.

Participants will learn how AALpy can be used to infer and validate deterministic, non-deterministic, and stochastic models. After demonstrating the automated testing of Python classes, we will discuss more advanced applications, including protocol fuzzing (e.g., MQTT, Bluetooth) and the extraction of interpretable models from recurrent neural networks.

In addition to active learning algorithms, we will also cover passive learning algorithms that have recently been added to AALpy.

Prof. Sir Charles Antony Richard (Tony) Hoare (1934-2026) was a giant of computer science, whose work bridged the gap between the abstract elegance of mathematical logic and the practical necessity of reliable software. Best known for the Quicksort algorithm, the development of Hoare logic, and the formalization of Communicating Sequential Processes (CSP), his career was defined by a relentless pursuit of "correctness by construction". This talk chronicles his journey from a student of the Classics at Oxford to the recipient of the ACM A.M. Turing Award, exploring a legacy that helped to transform programming from a craft into a disciplined science.

Formal program specifications provide a precise semantic foundation for understanding, generating, and verifying software. However, current large language models are still primarily evaluated and used through code-level tasks, while their ability to understand program semantics, produce rigorous specifications, and support end-to-end verification remains insufficiently explored. This talk presents a specification-centric perspective that connects these three challenges into a unified story. We first introduce formal specifications as semantic probes for evaluating code comprehension in LLMs, where specification judgement, selection, infilling, and generation tasks are used to examine whether models can capture program behaviours beyond individual execution traces. Building on this understanding-oriented view, we then present SpecGen, an LLM-based approach that generates formal specifications through conversational prompting, verifier feedback, and mutation-based refinement, aiming to produce specifications that accurately describe program behaviours. Finally, we introduce SpecSyn, which extends specification generation toward real-world program verification by decomposing large programs, synthesising segment-level specifications, and refining their semantic strength through non-equivalent program mutations and variant discrimination. Together, these works form a complete pipeline from specification-based semantic understanding, to automated specification generation, and further to verification-oriented specification synthesis, showing how formal specifications can serve as a bridge between LLM-based software intelligence and trustworthy program verification.

Abstract interpretation provides a generic framework for design static analysis, and has been widely applied in analysis of real-world programs. The scalability and precision of these analyses depend largely on the chosen abstract domain. The template polyhedral domain is well-known for offering a compelling trade-off between scalability and precision. However, designing effective templates currently requires intensive manual effort and domain expertise. This talk presents an approach to automatically generate linear templates for the template polyhedral domain. Experimental results demonstrate that our method can generate highly relevant templates for a variety of standard benchmark sets and complex real-world programs.

Formal synthesis has always been an important research direction in the field of automatic software generation, yet improving synthesis efficiency remains a major challenge. In recent years, LLM-based ode generation has been widely accepted, but how to generate high-quality code has drawn significant attention. For high-confidence Human-Cyber-Physical System (HCPS), its software generation must consider the correctness and safety of interactions between various entities and the external environment, and also needs to improve the quality of the generated code. This course introduces basic concepts of reactive synthesis, and our recent work on scaling up synthesis and improving efficiency, as well as LLM-based approaches for high-assurance code generation. We consider both formal and intelligent program synthesis to enhance the efficiency of automated development of HCPS software.

Digital twins are model-centric systems able to perform online analysis. These systems have become an important backbone for modern industry. The purpose of the digital twin is typically to help a target system meet requirements in an environment that it does not fully understand or control. The digital twin mirrors its target system in real time by integrating live observations of the target system, such as sensor data, into its knowledge. This allows the twin to assess the precision of its models, to adjust the models to make them more precise, and possibly to replace models or requirements on the fly to adapt to changes in the twinned system. Digital twins can be used for different kinds of analysis: descriptive analysis aims at explaining incidents that have happened, such as safety violations, predictive analysis aims at explaining what we expect will happen in the near future, thereby enabling a feedback loop to make adjustments to the target system, while prescriptive analysis explores hypothetical "what-if" scenarios for longer-term decision making. In this lecture, we introduce central concepts of digital twins, discuss simple examples, and explore the idea of digital twins from a formal methods perspective, including how to design digital twins as self-adaptive model management systems. We discuss how digital twins can be used to enhance the trustworthiness of software systems, and measures to enhance the trustworthiness of the digital twin itself.

Compilers serve as the fundamental infrastructure of the software and information industry. With the evolution of technology, conventional compilers such as GCC and LLVM can no longer meet the diverse emerging demands for trustworthiness, intelligence and other requirements in new application scenarios including aviation, aerospace and robotics. This report first elaborates on the concept of compiler trustworthiness for lightweight compilers and introduces mainstream trustworthy compilers. On this basis, it presents compiler testing methods designed to improve the quality of large-scale compilers. Finally, the report introduces a novel intelligent compiler developed by the research group, which is tailored for autonomous unmanned scenarios.

Timed automata and priced timed automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has developed a number of methods allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL CORA providing efficient support for optimization, Also the branch UPPAAL SMC, provides a highly scalable new engine supporting (parallel and distributed) statistical model checking of stochastic hybrid automata with significant applications to performance of energy-aware sensor networks as well as evaluation of lock-down measures in Denmark under COVID.

More recently the new branch UPPAAL Stratego offers a neuro-symbolic approach to achieve safe and near-optimal decision tree control strategies. The tool combines a dynamic partition-refinement Q-learning algorithm with symbolic methods for synthesizing safety shields that ensures correctness by design. To make synthesis of shields tractable, UPPAAL Stratego are using various abstraction and state-space transformation techniques. We demonstrate superiority of applying the shield before learning (pre-shielding) compared to after (post-shielding). In addition trade-offs between efficiency of strategy representation and degree of optimality subject to safety constraints will be discussed, as well as successful on-going applications (water-management, heating systems, and traffic control, swarm robotics). Most recently, methods for shielding and reinforcement learning has been extended to multi-agent systems.

Finally, the lecture will also cover a recent series of work on developing efficient methods for on-line monitoring the conformance of a real-time systems with respect to logical specifications (e.g. MITL). Most of the methods and techniques presented are to be found in the recently released UPPAAL 5.0

Model-driven development involves multiple heterogeneous artefacts, such as requirements, models, and code, as well as a variety of analyses, including testing, simulation, and formal verification. However, analyses are typically treated as secondary processes, and consistency is often checked only at a syntactic level, making it difficult to ensure meaningful system-level correctness as systems evolve. This talk presents a unified perspective that addresses both challenges. We first introduce the idea of analyses as first-class citizens, explicitly specified by their inputs, assumptions, outputs, and the properties they ensure. This enables modularisation, explicit dependency management, and efficient incremental re-execution when artefacts change. Building on this foundation, we then introduce an observable-centric approach to semantic consistency checking. Observables serve as shared, cross-domain properties that link requirements and models, allowing consistency constraints to be expressed and verified at a semantic level. By integrating these two perspectives, we obtain a framework in which analyses are both structurally explicit and semantically grounded.

Autonomous systems are distributed systems composed of agents, each pursuing its own goals, but which must coordinate to satisfy the overall goals of the system.

Main points covered:
1. We analyze the characteristics of autonomous systems, explaining that they underlie a multifaceted concept of intelligence that cannot be characterized by conversational behavioral tests such as the Turing test.
2. We propose a development method based on an agent reference architecture that characterizes autonomous behavior as the result of the composition of a set of independent functions. The behavior results from the orchestration of reactive behavior producing actions in response to external stimuli, and proactive behavior aimed at satisfying the agent's needs relating to the success of its mission. The two behaviors coordinate by sharing knowledge contained in a long-term memory.
3. We analyze how AI can contribute to the creation of AI agents and multi-agent systems, highlighting the need for its seamless integration with traditional software and discussing the current limitations of the state of the art. These limitations particularly concern the use of knowledge stored in long-term memory to semantically control and further improve the accuracy of AI components and adaptation to a constantly changing environment through goal management and planning.

We conclude by emphasizing that AI is still in its infancy, and that there is a long way to go to realize the vision of autonomous systems and get as close as possible to human intelligence.

Large language models (LLMs) are increasingly tasked with generating structured outputs. While structured generation methods ensure validity, they often lack output diversity, a critical limitation that we confirm in our preliminary study. We propose a novel method to enhance diversity in automaton-based structured generation. Our approach utilizes automata traversal history to steer LLMs towards novel structural patterns. Evaluations show our method significantly improves structural and content diversity while maintaining comparable generation efficiency. Furthermore, we conduct a case study showcasing the effectiveness of our method in generating diverse test cases for testing open-source libraries.

The question "Are AI minds genuine minds?" invites us to examine the nature of mind itself and whether artificial intelligence meets its defining criteria. A genuine mind is typically associated with consciousness, self-awareness, intentionality, and the capacity to experience mental states such as emotions. Whether AI qualifies as possessing a true mind ultimately depends on how we define the essential qualities of consciousness and intelligence. While this question has already been raised in the 19th Century, recent progress in AI requires us to re-examine it deeply.

FIRRTL is an intermediate representation language for Register Transfer Level (RTL) hardware designs. In FIRRTL programs, the bit widths of some components may not be given explicitly, thus they must be inferred during compilation. In mainstream FIRRTL compilers such as firtool, the width inference is conducted by a compilation pass called InferWidths, which may fail even for simple FIRRTL programs. In this paper, we investigate the width inference problem for FIRRTL programs. We show that if the constraint obtained from a FIRRTL program is satisfiable, there must exist a unique least solution. Based on this result, we propose a complete procedure for solving the width inference problem, which can handle programs while firtool may fail. We implement the procedure in Rocq and prove its correctness. From the Rocq implementation, we extract an OCaml implementation, which is the first formally verified InferWidths pass. Extensive experiments demonstrate that it can solve more instances than the official InferWidths pass in firtool using less time.

Heterogeneous programming design is programming crossing two or more languages. In this talk, we would like to share some trials on code transformation and memory leak detection crossing different languages. The techniques in use are immature. We share some challenges and thoughts in our work.

This series of lectures will explore how formal methods can be used to ensure the safety and reliability of modern complex systems, including systems that incorporate machine learning components. Automated reasoning plays a central role in the formal verification of hardware, software, and increasingly AI-based systems. As verification tools become more complex, certification techniques have been developed to provide an additional layer of trust in their results by producing independently checkable evidence of correctness. First, we will study static verification using automated reasoning such as SAT/SMT solving technologies, where certificates serve as mathematical proofs that allow verification results to be independently validated. Second, we will explore how reinforcement learning can be combined with formal methods to synthesize controllers and neural certificates for systems that are difficult to address with classical control techniques, while still providing formal guarantees with respect to temporal specifications. Third, we will study runtime monitoring and enforcement techniques, which provide runtime assurance as a complementary approach to static verification by detecting or preventing violations during system execution thereby enabling safe deployment of AI technologies in safety-critical applications.

Timed systems are widely deployed in industrial systems, especially in safety-critical domains. Formal verification is an important technique for ensuring the reliability of such systems, where model construction is crucial for subsequent analysis. Model learning can infer formal models from system behaviors and has been widely applied in areas such as protocol verification and embedded software analysis. In this course, we present related work on the modelling and verification of such systems.