Lectures

Manfred Broy, TU Munich
Modular Specification, Composition, and Refinement of Concurrent Interactive Systems
A theory and methodology is introduced for the systematic development of concurrent systems by formal techniques with emphasis on their architecture and functional abstraction. The interface behavior of interactive system is specified by interface predicates. Based on an operational semantics in terms of generalized Moore machines and its abstraction, a refinement calculus is introduced for interface specification including strong causality and full realizability. The concurrent composition of systems in terms of their interface behaviors is defined by logical conjunction. This way a system description technique is obtained that is compositional and modular, following the principles of encapsulation, information hiding, and modularity. A calculus is outlined which is sound and relative complete. Real time system behaviors are related to and abstracted into untimed system behaviors. Properties of untimed system behaviors are discussed. The role of time is discussion, being critical for real time systems and essential for identifying computational fixpoints for feedback loops. All concepts are illustrated by a simple, but practically relevant running example.

Cristian Cadar, Imperial College London
Introduction to Dynamic Symbolic Execution and KLEE Cristian Cadar, Imperial College London

 Dynamic symbolic execution has gathered a lot of attention in recent years as a key ingredient in areas including  software engineering, programming languages, program verification, cybersecurity, and computer systems.  Dynamic symbolic execution has enabled a wide range of applications such as high-coverage test suite generation, bug and security vulnerability detection, patch testing, automatic debugging, program repair, and more.

 In this tutorial-style presentation, I will introduce the main concepts of dynamic symbolic execution and exemplify them in the context of the KLEE symbolic execution infrastructure (https://klee-se.org/), a popular system with a large user base across academia and industry.

The talk is primarily targeted to those who have no direct experience with dynamic symbolic execution and KLEE, but the talk will also include several parts useful to a more specialist audience.

Marsha Chechik, University of Toronto
Elicitation and Formal Reasoning about Normative Requirements
Abstract: As software and cyber-physical systems interacting with humans become prevalent in domains such as healthcare, education and customer service, software engineers need to consider normative (i.e., social, legal, ethical, empathetic and cultural) requirements. However, their elicitation is challenging, as they must reflect the often conflicting or redundant views of stakeholders ranging from users and operators to lawyers, ethicists and regulators. I will describe a tool-supported framework for normative requirements elicitation. Built on top of LEGOS-a custom bounded satisfiability checker for first order logic with transitive closure, our framework allows specification of normative rules for a software system in an intuitive high-level language called SLEEC, and provides automated analysis to identify rule conflicts, redundancies, and other well-formedness concerns. It also synthesizes feedback enabling users to understand and resolve problems. Our approach has been successfully applied to over a dozen realistic case studies from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots, and supported teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers.

Sumit Gulwani, Microsoft, Redmond
AI-assisted Programming: Applications, Experiences, and Neuro-symbolic techniques
AI can enhance programming experiences for a diverse set of programmers. This includes professional developers and data scientists who require assistance in software engineering and data wrangling, spreadsheet users who need help authoring formulas, and students seeking guidance on programming homework. Users can express their intent explicitly through input-output examples or natural language specifications, or implicitly by presenting bugs or recent code edits.
The task of synthesizing an intended program snippet from the user’s intent is both a search and a ranking problem. Search is required to discover candidate programs that correspond to the (often ambiguous) intent, and ranking is required to pick the best program from multiple plausible alternatives. This creates a fertile playground for combining symbolic-reasoning techniques, which can model the semantics of programming operators, and machine-learning techniques, which can model human preferences in programming. The emergence of large language models (LLMs), as a very powerful general-purpose tool and especially for programming tasks, have been a boon to this field. While LLMs are not very precise by themselves, they provide a very flexible surface for implementing a variety of cognitive strategies that enable construction of more robust neuro-symbolic AI systems.
Finally, a few critical requirements in AI-assisted programming are usability, precision, and trust; and they create opportunities for innovative user experiences and interactivity paradigms. In these lectures, I will explain these concepts using some existing successes, including the Flash Fill feature in Excel, Data Connectors in PowerQuery, IntelliCode Suggestions in Visual Studio, and more recently various programming agents in Microsoft CoPilots. I will also describe several new opportunities in AI-assisted programming, which can drive the next set of foundational neuro-symbolic advances.

Laura Kovacs, TU Wien
First-Order Theorem Proving
First-order theorem proving is one of the earliest research areas within artificial intelligence and formal methods. It is undergoing a rapid development thanks to its successful use in program analysis and verification, security analysis, symbolic computation, theorem proving in mathematics, and other related areas. Breakthrough results in all areas of theorem proving have been obtained, including improvements in theory, implementation, and the development of powerful theorem proving tools. However, recent developments are not always easily accessible to non-specialists.
This mini-lecture series presents the theory and practice behind the development of powerful theorem proving tools.  The workhorse used for a demonstration of concepts discussed at the tutorial will be our theorem prover Vampire.
The tutorial will first focus on practicalities while using first-order Vampire for validating mathematical theorems. We will then  further introduce the core concepts of automating first-order theorem proving in first-order logic with equality. We will discuss the resolution and superposition calculus, introduce the saturation principle, present various algorithms implementing redundancy elimination, and demonstrate how these concepts are implemented in Vampire.

Rustan Leino, Amazon Web Services
Induction in deductive reasoning

Understanding how to prove the correctness of a program is an essential ingredient in a software engineer's tool box. In these lectures, I will build from the basics of deductive program proofs to techniques that can be implemented in an automated program verifier. A common theme will be how to layer one proof on top of others, and in particular layering one proof on top of smaller instances of itself. This is known as induction or recursion. I will explain the reusable core idea of induction using a well-founded order, and will show how it not only solves a variety of proof problems, but also can be automated.

Anders Møller, Aarhus University
Static Program Analysis

Static program analysis is the art of reasoning about the behavior of computer programs without actually running them. This is useful not only in optimizing compilers for producing efficient code but also for automatic error detection and other tools that can help programmers. Many software companies increasingly use static program analysis for preventing security vulnerabilities. This series of lectures will present essential principles and algorithms for static program analysis, based on material from https://cs.au.dk/~amoeller/spa/. The topics include basic dataflow analysis, interprocedural analysis, pointer analysis, control-flow analysis, and an introduction to the theory of abstract interpretation.

Peter Müller, ETH Zurich
Ownership in Program Verification - From Separation Logic to Rust and Back

Imperative programs are notoriously difficult to reason about. Shared mutable state may lead to subtle interactions between program components and cause memory errors, unintended side effects, data races, and other bugs. 

Ownership is a powerful concept to track which memory locations are exclusively owned (and can thus be safely mutated) and which ones may be shared (and should thus be immutable). It enables the modular verification of heap-manipulating programs in Separation Logic and is the foundation of Rust's powerful type system, which eliminates memory errors statically.

This lecture series will provide an overview of ownership-based verification in the Viper system and introduce Rust's ownership type system. It will explain how Rust facilitates verification by extracting memory safety proofs automatically from the type information, which can then be extended easily to verify stronger program properties.

Frank Piessens, KU Leuven
Software security across abstraction layers

This lecture series provides an advanced introduction to the field of software security. We first define the key concepts of the field, and we look at old and new examples of software security failures. A particularly challenging and intriguing aspect of software security is that functionality of software and desired security properties are often formulated most naturally at a relatively high level of abstraction, but attacks commonly exploit implementation details at lower levels of abstraction. We discuss in detail how software that is in theory secure at one level of abstraction (sometimes even provably secure) can be broken in practice by attacking a lower abstraction layer. One example class of attacks that we discuss in detail are transient execution attacks. These attacks break confidentiality properties of software by exploiting performance optimization mechanisms in processors. With an understanding of the attacks in mind, we reconsider the problem of proving the security of software systems, and discuss an approach to prove software confidentiality properties while considering attacks at multiple abstraction layers. But we also discuss the fundamental limitations of provable security, and the important complementary role that attack research can play.

Alexander Pretschner, TU München and fortiss
Scenario-Based Tests for Cyber-Physical Systems

We present several results on scenario-based testing, an equivalence class testing method typically applied to (autonomous) cyber-physical systems. We first recap how to generate tests by translating scenario descriptions into optimization problems. We then show that randomly sampling as well as re-using tests in general is problematic and that instead, new tests need to be generated for each new version of the systems, at least in principle - and this is prohibitive. We suggest a way to overcome this problem. Using the example of UAVs, we discuss empirical results on the power of heuristic search and show that different search algorithms lead to largely different results—with some generated test suites finding safety-critical behavior and some failing to do so. Moreover, we show how to create linguistic scenario descriptions from clustered recorded drives and, specifically, show how to validate the quality of these descriptions. Finally, we present different dimensions of and criteria for the completeness of scenario-based test suites.

Zach Tatlock, University of Washington
Exploring Optimization and Analysis with EqSat in egglog
Term rewriting enables implementing complex transformations as a sequence of simple, syntactic rewrites; this has made it a foundational technique in program optimization, synthesis, and verification. However, orchestrating rewrites effectively poses significant challenges: in what order should we run rewrite rules? Equality Saturation (EqSat) is a technique that approximates running all the rules in every order. Naively, this should obviously ``blow up'' combinatorially, but EqSat uses the equality graph (e-graph) data structure from congruence closure algorithms to efficiently represent large sets of equivalent subterms.
Our group has developed egg and egglog, general Equality Saturation (EqSat) frameworks, designed to streamline the process of code transformation and analysis. These frameworks have quickly gained traction in various domains, including ML kernel optimization, circuit design tools, 3D CAD editors, and more. In this lecture series, we will delve into the design principles of egglog and highlight recent advancements that have enhanced its performance, expressiveness, and proof generation capabilities. Specifically, we will explore how techniques borrowed from relational databases have made egglog simpler, more expressive, and faster. By integrating domain-specific analyses and transformations, egglog also goes beyond traditional syntactic rewriting. The lectures will provide hands-on experience with egglog, survey the evolution of EqSat and the egglog framework, detail key design decisions, and survey the emerging theoretical results around EqSat. See more at https://egraphs-good.github.io/

Cesare Tinelli, University of Iowa
Modeling and analyzing reactive systems with logic-based symbolic model checkers

Model-based software development is a leading methodology for the construction of safety- and mission-critical embedded systems. Formal models of such systems can be validated, via formal verification or testing, against system-level requirements and modified as needed before the actual system is built. In many cases, source code can be even produced automatically from the model once the system designer is satisfied with it. As embedded systems become increasingly large and sophisticated, the size and complexity of models grows correspondingly, making the verification of system requirements harder, especially in the case of infinite-state systems.

This lecture series introduce a modeling language and verification environment for specifying and statically analyzing a variety of reactive computational systems. The specification language is an extension of Lustre, a declarative and synchronous dataflow programming language. The verification environment is built around the Kind 2 model checker and supports high-level modeling features such as assume-guaranteed contracts and mode-based specifications, which enable the modular and compositional verification of multi-component systems. The lectures will focus on the specification and verification of safety properties but discuss also additional kinds of analysis important in industrial applications such as contract realizability checking, merit analysis and blame analysis. They will conclude with a general description of the main automated reasoning techniques used under the hood to enable such analyses.