Reactive synthesis is the automatic construction of reactive systems from high-level formal specifications, guaranteeing correctness by design. Reactive systems continuously interact with potentially adversarial environments—examples include software controllers for robotic platforms or embedded systems. Many real-world applications involve infinite-state models due to the presence of unbounded data types such as integers. This makes the synthesis problem undecidable in general and highly challenging in practice.

In this course, we will explore the theoretical foundations and state-of-the-art techniques for the synthesis of reactive systems over infinite data domains. We will introduce specification formalisms based on temporal logics and two-player games, and discuss the subtleties involved in writing specifications that accurately reflect the designer's intent. There are two prominent classes of approaches to the synthesis of infinite-state reactive systems. Abstraction-based methods abstract the synthesis problem to a finite-state one, to which classical techniques apply. Constraint-based techniques, on the other hand, work directly on a symbolic representation of the infinite-state problem. Our focus will be on the second class -- constraint-based techniques -- with particular attention to recently proposed techniques that integrate logical reasoning into the reactive synthesis procedures. The course includes hands-on exercises in writing specifications and applying the open-source tool Issy (https://github.com/phheim/issy).

This lecture explores how to build automatic verification tools that check whether a given program satisfies a given specification. Unlike deductive approaches, these tools do not require programs to be annotated with loop invariants and procedure contracts, though they may not terminate due to the undecidability of the verification problem. We examine key building blocks for such tools, particularly the CEGAR (Counterexample-Guided Abstraction Refinement) approach, which works with abstractions, analyzes potential counterexamples, and learns from spurious counterexamples to refine abstractions iteratively. The lecture focuses on trace abstraction, an automata-based verification approach implemented in the Ultimate program analysis framework. Trace abstraction utilizes various types of automata—including finite automata, Büchi automata, visibly pushdown automata, and Petri nets—enabling us to check temporal properties for sequential programs and analyze safety properties for concurrent programs. Through the Ultimate framework, we demonstrate how these theoretical foundations translate into a practical verification tool that can handle real-world C programs.

TBD

TLA+ is a language for formally describing algorithms and systems. It is based on mathematical set theory for describing the data that ana algorithm manipulates and on linear-time temporal logic for describing the executions of the algorithm. Properties of TLA+ specifications can be mechanically verified using the explicit-state model checker TLC, the symbolic model checker Apalache, and the interactive proof assistant TLAPS. In this hands-on tutorial we will introduce the language TLA+ and its support tools, discuss common specification idioms, and give hints on how to effectively verify TLA+ specifications.

Vampire is an award-winning automatic theorem prover for first-order logic, including support for theories. It is based on saturation, a state-of-the-art theorem proving technology, and employs the superposition calculus for efficient support of equational reasoning. Moreover, Vampire features the AVATAR architecture for clause splitting, allowing it to offload the propositional essence of the given problem to a dedicated SAT solver. The lecture will introduce theorem proving as a prime example of an automated reasoning task and outline the basic building blocks of Vampire, from theoretical foundations to implementation tricks and heuristics. Modern machine learning techniques can be used to boost these heuristics by allowing the prover to learn from past successes. The lecture will conclude with a hands-on session using Vampire, showcasing both its main functionalities and lesser-known features.