Modern distributed systems often partition and replicate the data they manage across a large number of nodes and a wide geographical span. A key challenge that such systems have to address is maintaining data consistency in the presence of concurrent modifications at different nodes and despite inevitable failures. There is a spectrum of consistency models that a system can provide, and navigating it is far from trivial. Strong consistency models give the programmer the illusion that all nodes are always in sync, but hinder system scalability. In contrast, weak consistency models expose the programmer to the effects of replication in exchange for more scalable implementations. We will present modern methods for formally specifying consistency models of distributed systems and reasoning about how their choice affects system correctness. We will also present techniques for proving the correctness of consistency model implementations, including Paxos-based replication and replicated data types.

[Slides]

The Ultimate goal of software model checking is push button verification of existing code. In an ideal world one would use model checkers to find generic errors in code, e.g., undefined behaviour or crashes, similar to the way compilers today can be used to find syntactical errors. While this goal cannot be perfectly achieved the problem in general is undecidable the problem can be decided in common cases.

In this lecture we will take a closer look into a particular software model checker, Ultimate Automizer. This tool aims to be a sound verification tool that either finds a concrete error, proves the absence of errors, or runs out of resources. We will explain how the problem of finding generic errors on C programs can be reduced to a reachability problem in a simpler language. We will look under the hood and investigate techniques like trace abstraction and interpolation based model checking. This will be illustrated with examples where this method succeeds to prove the program correct and we show the limitations of this method.

[Slides]

F* is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, or C code. This enables verifying the functional correctness and security of realistic applications, such as a verified HTTPS stack.

This course will give an introduction to program verification in F* using simple examples and a few, even simpler exercises along the way. We will start with specifying and verifying purely-functional programs and then move to programs with side-effects such as divergence and mutable state. We will also cover F*’s support for reasoning about monotonically evolving state and for adding extra monadic side-effects, which is for instance used to implement F*’s tactic system in F* itself. Finally, we will look a bit under the hood at how F* encodes verification conditions to the SMT and how it computes them in the first place using monads indexed by predicate transformer monads, aka Dijkstra monads.

[Course Material]

Concurrent and distributed software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent or distributed program.

In this lecture, I present an approach based on program annotations. I will first describe the fundamental of annotation-based verification, and then I discuss what is needed to use this approach for concurrent and distributed software. In particular, for concurrent and distributed software the program annotations have to take care of what part of the memory is affected by a thread or process. To take care of this, the program annotations will be based on concurrent separation logic. I will describe how this is done, and how we support reasoning about concurrent and distributed programs using the VerCors tool set.

In the second part of the lecture, I will describe a further extension, which allows one to reason about behavioural properties of a concurrent or distributed program. We will show how we can define an abstract model that captures the behaviour of the program. We use program logic to show that the program behaves as described by the abstract model, while we use model checking to reason about properties of the abstract model.

Throughout the lecture, various exercises will be given, so that the audience gets hand-on experience with verification of concurrent and distributed software.

[Course Material]

The course will discuss the learning problems in theorem proving. We will start with the design of automated and interactive theorem proving systems as well as proof certifiers and discus the various machine learning problems that correspond to the built in heuristics. First, the course will focus on the high-level learning problems in proof assistants and techniques for the selection of relevant lemmas in large libraries. Next the focus of the course will be on strategy selection and strategy tuning using learning. Finally internal guidance of automated reasoning systems, including prediction of useful inference steps and tactics, as well as the evaluation of intermediate proof states will be discussed.

[Part1], [Part2]