Markov chains (MC) and Markov decision processes (MDP) are widely used as operational models for the quantitative system analysis. They can be understood as transition systems augmented with distributions for the states (in MC) or state-action pairs (in MDPs) to specify the probabilities for the successor states. Additionally one might add weight functions for modeling accumulated costs or rewards earned along path fragments to represent e.g. the energy consumption, the penality to be paid for missed deadlines, the gain for completing tasks successfully or the degree of the achieved utility.

The tutorial will introduce the main features of discrete-time, finite-state Markovian models (MC and MDP) and their quantitative analysis against temporal logic specifications. The first part will present the basic principles of the automata-based approach for linear temporal logic (LTL) and probabilistic computation tree logic (PCTL), including a summary of techniques that have been proposed to tackle the state-explosion problem. The second part of the tutorial will present algorithms for dealing with fairness assumptions and computing conditional probabilities and quantiles.

Many privacy and security properties are relational, in the sense that they relate two executions of a system, or the execution of an ideal system, which is secure by assumption, and a real system, for which security is sought. As a consequence, relational properties are an important target for program verification. The course will introduce probabilistic couplings, which are used in probability theory for analyzing Markov chains, and demonstrate that many relational properties of probabilistic programs are modelled by (generalized) probabilistic couplings. Then, it will present program logics for proving the existence of probabilistic couplings, and show applications to differential privacy and cryptography.

Many program verification, analysis, testing and synthesis queries reduce to solving satisfiability of logical formulas. Yet, there are several applications where satisfiability, and even a model or a proof, is insufficient. Examples of useful additional information include interpolants, models that satisfy optimality criteria, generating strategies for solving quantified formulas, enumerating and counting solutions. The lectures describe logical services from the point of view of the Satisfiability Modulo Theories solver Z3. We cover their foundations, algorithmics and ways to put these features to use.

F* is a verification-oriented programming language equipped with dependent types, programmable monadic effects, and a weakest precondition calculus. These features allow us to express precise and compact specifications for programs. The F* type-checker then tries to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be compiled to OCaml, F#, and (more recently) to C for execution.

The main ongoing use case of F* is to build a verified, efficient, drop-in replacement for the HTTPS stack. So far, this includes implementations of the TLS Internet Standard and of its underlying cryptographic algorithms and constructions.

In these lectures, I will give an overview of programming & verification in F* based on security examples, ranging from functional correctness for optimized implementations of cryptographic algorithms to cryptographic proofs of security for (fragments of) TLS 1.3.

See https://fstar-lang.org/ for an online tutorial and research papers describing the latest features of F*. See https://project-everest.github.io/ for its security application to TLS and HTTPS.

In the process of software production and maintenance, much effort and many resources are invested in order to ensure that the product is as bug free as possible. Manual bug repair is time-consuming and requires close acquaintance with the checked program. Therefore, there is a great need for tools performing automated program repair.

Many works are aimed at developing program repair tools which enable auto- matic repair of real-world bugs found in large-scale software projects. As a result, they are targeted for the type of bugs found in deployed real-world software.

Our repair algorithm, on the other hand, is designed for assisting the developer in early stages of developments. Our goal is to have a fast, easy-to-use program repair tool, which programmers can run routinely. Ideally, programmers will run the tool immediately after making changes to the program, before any manual effort was invested in debugging at all.

We use a bounded notion of correctness. We say that a program is repaired if whenever a bounded computation reaches an assertion, the assertion is evaluated to true. Our repair method is sound, meaning that, every returned program is repaired. Just like Bounded Model Checking, this increases our confidence in the returned program.

Our programs are repaired using a predefined set of mutations, applied to expressions in conditionals and assignments (e.g. replacing a + operator by a −). We impose no assumptions on the number of mutations needed to repair the program and are able to produce repairs involving multiple buggy locations, possibly co-dependent.

To make sure that our suggested repairs are as close to the original program as possible, the repaired programs are examined and returned in increasing number of mutations. In addition, only minimal sets of mutations are taken into account. Our method is complete in the sense of returning all minimal sets of mutations that create a repaired program.

The choice to use mutations for repair makes the search space small enough to enable completeness at an affordable cost, yet it is expressive enough to repair meaningful bugs (especially those present in earlier stages of development).

Our algorithm is based on the translation of the program into a set of SMT constraints which is satisfiable iff the program contains an assertion violation. This was originally done for the purpose of Bounded Model Checking in [2].Thus, searching the space of mutated programs is reduced to searching unsatisfiable sets of constraints. We show how to perform the latter efficiently using a sophis- ticated cooperation between SAT and SMT solvers.

Probabilistic programming is en vogue. It is used to describe complex Bayesian networks, quantum programs, security protocols and biological systems. Programming languages like C, C#, Java, Prolog, Scala, etc. all have their probabilistic version. Key features are random sampling and means to adjust distributions based on obtained information from system observations. We show some semantic intricacies, argue that termination is more involved than the halting problem, and discuss recursion and run-time analysis.

We first give a brief overview of program analysis methods, with an emphasis on the relative strengths and weaknesses of dynamic and static analyses, and under- vs. over-approximative methods. We then explain how low-level exploits are orchestrated, and illustrate this with a few practical examples. We then discuss how program analysis methods can be applied to automate the search for functional exploits, and attempt a scientific approach towards evaluating alternative analysis techniques. We will discuss bounded model checking, path-based symbolic simulation, and abstraction techniques.

In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification against all environments. The short course introduces the synthesis problem for specifications given by linear-temporal logic (LTL) formulas, algorithms for solving it, its complexity, and recent ideas in making synthesis useful in practice. The course assumes no previous knowledge. We will define LTL, automata on infinite words, two-player games, and transducers, and will learn how they serve as a basis for the formal definition and solutions of the synthesis problem.

This series of four lectures will provide an introduction to compiler verification for ML-like functional programming languages. In particular, the lectures will cover topics such as: (1) how to setup a compiler verification proof, i.e. the semantics of programming languages and the theorem statements; (2) how to verify the compilation of the data abstraction that functional languages provide; (3) how to implement and verify compilation of (curried) closure applications; (4) and finally how a verified compiler can be bootstrapped in the logic of an interactive theorem prover. Many of the examples will be based on the CakeML compiler which has been verified and bootstrapped in the HOL theorem prover.

This series of lectures is concerned with data structures for functional programming languages and with the formal verification of their functional correctness and their complexity. A number of more and less well known data structures will be examined and it will be shown that a theorem prover (here: Isabelle) is a suitable environment for proving not just functional correctness but also for analyzing the (amortized) complexity of algorithms. The focus will be on search trees and priority queues.

Formal verification technology is widely deployed, different proof technologies occupying largely separate spheres. SMT solvers combine linear arithmetic and other decision procedures with simple logic, while interactive theorem provers allow the editing of large specifications and resolution theorem provers solve hard problems in pure first-order logic. However, real world problems require a combination of verification technologies.

Hybrid systems have a digital control but continuous behaviour. For example, a thermostat switches on or off according to the current temperature, which will then rise or fall continuously. Other applications may involve acceleration or the opening of valves; in each case the continuous behaviour is described by a differential equation and approximated by a formula involving the special functions sin, cos, exp, ln, etc.

MetiTarski is an automatic theorem prover for verifying inequalities involving such functions. It combines classical resolution, decision procedures for polynomial problems and axiomatic information about special functions. In addition, MetiTarski contains specialised code to put formulas into a canonical form, and a modified term ordering; these cooperate to create a search space in which occurrences of special functions are successively eliminated.

The lectures will examine this architecture in detail, with the aim of suggesting new ways of combining resolution with decision procedures. They will cover classical resolution and in particular ordered resolution (or superposition), which uses an ordering to constrain the search by selecting a particular literal. They will describe a method of integrating decision procedure calls with resolution at a low level. They will examine refinements specific to MetiTarski, such the Knuth-Bendix term ordering and necessary modifications to it. Applications of MetiTarski to hybrid systems will also be covered. Finally, we can ask how to integrate such techniques with other verification tools.

Dynamic logic has been introduced for understanding programs, but its real calling are dynamical systems. Dynamic logic excels at providing simple and elegant logical foundations for the dynamical systems arising in cyber-physical systems. Since these CPSs combine cyber aspects such as communication and computer control with physical aspects such as movement in space, their dynamical system models also combine discrete dynamics with continuous dynamics. Differential dynamic logic provides a programming language for these models and comes with a compositional axiomatization. Its implementation in the KeYmaera X theorem prover has been instrumental in verifying applications such as the Airborne Collision Avoidance System ACAS X and ground robot navigation. This series of lectures will additionally consider differential game logic for hybrid games , which add an adversarial element to the dynamics.