Lecturers

MIKOŁAJ BOJAŃCZYK (University of Warsaw)

Computation Theory with Atoms

This course will survey applications of sets with atoms to automata, language and computation theory. We will study various properties that can be expected from the structure of data atoms and the impact of those properties on concepts such as orbit-finiteness, definable sets and notions of computability. The presentation will roughly follow significant parts of the forthcoming book. https://www.mimuw.edu.pl/~bojan/paper/atom-book.

Link to the recording of the talk

Slides part-1, part-2, part-3

DMITRY CHISTIKOV (University of Warwick)

Ultimately periodic sets, semi-linear sets, and Presburger arithmetic

How to generalize ultimately periodic sets of natural numbers to several dimensions? An answer to this question is the definition of semi-linear sets. These sets coincide with the sets definable in Presburger arithmetic, the first-order theory of the natural numbers with addition and order, and have numerous applications in the foundations of verification. In this short tutorial, I will give an introduction to semi-linear sets and Presburger arithmetic, illustrating several classic techniques as well as recent developments. In particular, we will look at the geometry of sets of solutions to linear Diophantine inequalities and review the complexity of related computational problems.

Link to the recording of the talk

Slides

THAO DANG (Verimag and CNRS)

Set-based computation for hybrid systems verification

Reachability analysis has become a de facto approach for formal verification of hybrid systems. Exact reachable set computation is impossible for most non-trivial hybrid systems, and alternatively, much research has focused on developing set representations that can be efficiently manipulated to compute sufficiently accurate over-approximation of the reachable set. In this presentation, we will show a number of well-known set representations and how to perform operations on them to verify important properties such as safety and stability.

Link to the recording of the talk

JAVIER ESPARZA (TU München)

Proving liveness properties of replicated systems

Replicated systems consist of a finite-state program that is executed by an unknown number of indistinguishable agents, communicating by rendez-vous or via shared variables. Examples include distributed protocols and multithreaded programs, or abstractions thereof. Verifying a replicated system amounts to proving that an infinite family of systems satisfies a given property. This is already a formidable challenge, but it is made even more difficult by the fact that correctness problems for distributed protocols require to check liveness properties against a class of schedulers. Indeed, liveness properties are known to be harder to verify than safety properties, and scheduling adds additional problems. We address the verification of liveness properties of replicated systems with stochastic scheduling. We present both theoretical results and a tool built on top of a solver for integer linear constraints.

Link to the recording of the talk

ANTHONY LIN (TU Kaiserslautern)

Algorithmic Verification of String-Manipulating Programs

Strings are among the most fundamental and commonly used data types in modern programming languages. Heavy string manipulations in programs often lead to mistakes, some of which could have serious security consequences (e.g. cross-site scripting). This gives rise to the currently active research area of algorithmic verification of string-manipulating programs. As is standard in software model checking, one crucial problem is to come up with an appropriate string theory and a decision procedure for it. This is because in theory a software model checker could then use standard methods (e.g. symbolic execution) to lift the decision procedure from formulas to programs. In this talk, I will describe the challenges of the design of a good string theory and decision procedure for the theory, as well as some existing attempts towards them. In particular, this is a tricky problem because there are many string operations that one would like to include as a primitive operation (especially from the point of view of techniques like symbolic execution), but at the same time they easily lead to undecidability.

Link to the recording of the talk

Slides

DEJAN NICKOVIC (AIT Vienna)

From real-time temporal logic to timed automata

We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer which inputs a signal holding the Boolean value of atomic propositions, and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities, and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.

Link to the recording of the talk

JEAN-FRANCOIS RASKIN (Université Libre de Bruxelles)

Two-Player Zero Sum Games played on Graphs

The class of two-player zero sum games played on graphs is a canonical model to formalize and reason about the non-terminating interaction between a system and its environment. In this series of lectures, I will expose fundamental results for game graphs both for omega-regular objectives and for quantitative objectives. Those results will cover algorithms and complexity analysis of the central problems in the area.

Link to the recording of the talk

ANDREW REYNOLDS (University of Iowa)

Solving Verification Conditions using SMT Solvers

A growing number of approaches to software and hardware verification use Satisfiability Modulo Theories (SMT) solvers as backend reasoning engines. SMT solvers have gained significant popularity due to their ability to efficiently reason in combinations of theories such as arithmetic, arrays, inductive datatypes and unbounded character strings. This talk will cover the DPLL(T) solving architecture on which SMT solvers are based, and give simple examples of how they can be used for discharging verification conditions from various applications.

Link to the recording of the talk

Slides

ALEXANDRA SILVA (University College London)

Programming and Reasoning with Kleene Algebra with Tests

Computer scientists have long explored the connections between families of programming languages and abstract machines. This dual perspective has furnished deep theoretical insights as well as practical tools. As an example, Kleene’s classic result establishing the equivalence of regular expressions and finite automata inspired decades of work across a variety of areas including programming language design, mathematical semantics, and formal verification. Kleene Algebra with Tests (KAT), which combines Kleene Algebra (KA) with Boolean Algebra (BA), is a modern example of this approach. Viewed from the program-centric perspective, a KAT models the fundamental constructs that arise in programs: sequencing, branching, iteration, non-determinism, etc. The equational theory of KAT enables algebraic reasoning and can be finitely axiomatized. Viewed from the machine-centric perspective, a KAT describes a kind of automaton that generates a regular language of traces. This shift in perspective admits techniques from the theory of coalgebras for reasoning about program behavior. In particular, there are efficient algorithms for checking bisimulation, which can be optimized using properties of bisimulations or symbolic automata representations. KAT has been used to model computation across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, and more. A prominent recent application is NetKAT, a language for reasoning about the packet-forwarding behavior of software-defined networks. NetKAT has a sound and complete equational theory, and a coalgebraic decision procedure that can be used to automatically verify properties such as reachability, loop-freedom, and isolation. The main objective of this tutorial is to provide attendees with a comprehensive introduction to Kleene Algebra with Tests (KAT) including techniques for using KAT to model and reason about computation in a variety of domains. This is based on joint work and previous tutorials with Nate Foster and Dexter Kozen (Cornell University).

Link to the recording of the talk

Slides

JAMES WORELL (University of Oxford)

Decision Problems for Linear Dynamical Systems

Linear dynamical systems occur throughout theoretical computer science, including in automata theory, hybrid systems, and software verification. This tutorial will introduce several decision problems in linear dynamical systems that are variously connected with threshold problems in automata theory, loop termination in software analysis, and reachability and liveness in hybrid systems. Our aim is describe some of the history of these problems, to describe the current frontier of decidability, and to introduce relevant mathematical tools–algebraic and number-theoretic–for analysing the problems.

Link to the recording of the talk

Slides