ABSTRACT. In this tutorial on active automata learning algorithms, I will start with the famous L* algorithm proposed by Dana Angluin in 1987, and explain how this algorithm approximates the Nerode congruence by means of refinement. Next, I will present a brief overview of the various improvements of the L^* algorithm that have been proposed over the years. Finally, I will introduce L#, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the L* algorithm and its descendants, L# takes a different perspective: it tries to establish apartness, a constructive form of inequality.

ABSTRACT. Stainless ( https://stainless.epfl.ch ) is an open-source tool for verifying and finding errors in programs written in the Scala programming language. This tutorial will not assume any knowledge of Scala. It aims to get first-time users started with verification tasks by introducing the language, providing modelling and verification tips, and giving a glimpse of the tool's inner workings (encoding into functional programs, function unfolding, and using theories of satisfiability modulo theory solvers Z3 and CVC4).

Stainless (and its predecessor, Leon) has been developed primarily in the EPFL's Laboratory for Automated Reasoning and Analysis in the period from 2011-2021. Its core specification and implementation language are typed recursive higher-order functional programs (imperative programs are also supported by automated translation to their functional semantics). Stainless can verify that functions are correct for all inputs with respect to provided preconditions and postconditions, it can prove that functions terminate (with optionally provided termination measure functions), and it can provide counter-examples to safety properties. Stainless enables users to write code that is both executed and verified using the same source files. Users can compile programs using the Scala compiler and run them on the JVM. For programs that adhere to certain discipline, users can generate source code in a small fragment of C and then use standard C compilers.

https://github.com/epfl-lara/fmcad2021tutorial

ABSTRACT. The automatic synthesis of reactive systems from high-level specifications is a highly attractive and increasingly viable alternative to manual system design, with applications in a number of domains such as robotic motion planning, control of autonomous systems, and development of communication protocols. The idea of asking the system designer to describe what the system should do instead of how exactly it does it, holds a great promise. However, providing the right formal specification of the desired behaviour of a system is a challenging task in itself. In practice it often happens that the system designer provides a specification that is unrealizable, that is, there is no implementation that satisfies it. Such situations typically arise because the desired behavior represents a trade-off between multiple conflicting requirements, or because crucial assumptions about the environment in which the system will execute are missing. Addressing such scenarios necessitates a shift towards synthesis algorithms that utilize quantitative measures of system correctness. In this tutorial I will discuss two recent advances in this research direction.

First, I will talk about the maximum realizability problem, where the input to the synthesis algorithm consists of a hard specification which must be satisfied by the synthesized system, and soft specifications which describe other desired, possibly prioritized properties, whose violation is acceptable. I will present a synthesis algorithm that maximizes a quantitative value associated with the soft specifications, while guaranteeing the satisfaction of the hard specification. In the second half of the tutorial I will present algorithms for synthesis in bounded environments, where a bound is associated with the sequences of input values produced by the environment. More concretely, these sequences consists of an initial prefix followed by a finite sequence repeated infinitely often, and satisfy the constraint that the sum of the lengths of the initial prefix and the loop does not exceed a given bound. I will also discuss the synthesis of approximate implementations from unrealizable specifications, which are guaranteed to satisfy the specification on at least a specified portion of the bounded-size input sequences. I will conclude by outlining some of the open avenues and challenges in quantitative synthesis from temporal logic specifications.

ABSTRACT. Smart contracts consist of distributed programs built over a blockchain and they are emerging as a disruptive paradigm to perform distributed computations in a secure and efficient way. Given their nature, however, program flaws may lead to dramatic financial losses and can be hard to fix. This motivates the need for formal methods that can provide smart contract developers with correctness and security guarantees, ideally automating the verification task.

This tutorial introduces the semantic foundations of smart contracts and reviews the state-of-the-art in the field, focusing in particular on the automated, sound, static analysis of Ethereum smart contracts. We will highlight the strengths and drawbacks of different methods, suggesting open challenges that can stimulate new research strands. Finally, we will overview eThor, an automated static analysis tool that we recently developed based on rigorous semantic foundations.