ICTAC 2019
Hammamet, Tunisia.
October 31 - November 4, 2019

Abstract interpretation aims at formalizing formal methods. This is illustrated by the design of verification and static analysis for a simple subset of C. We define the structural rule-based and then fixpoint prefix trace semantics of this simple subset of C. We define program properties and the strongest collecting semantics. We formalize the exact abstraction of program properties and how a structural rule-based/fixpoint abstract semantics can be derived from the collecting semantics by calculational design. This is applied to program verification methods and program logics which are (non-computable) abstractions of the program collecting semantics. Static analysis is based on the approximation of program properties. We introduce a few classical effectively computable abstractions of numerical properties of programs and shortly discuss industrial static analysis applications. We also consider a few abstractions of symbolic properties of programs and discuss opened problems.

The state explosion problem is the main obstacle for the verification of large scale concurrent systems, as they are generally based on an interleaving semantics, where all possible firing orders of concurrent actions are exhaustively explored. Different techniques for fighting this problem have been proposed. This tutorial presents partial order techniques which have been proven to be the most successful in practice. We first present the theoretical bases of the two classes of partial order techniques: partial order reduction techniques and step graph techniques. The common characteristics of all these methods is to reduce the state space to be explored, by selecting the actions or sets of actions (steps) to be executed from each state. The step graph methods aim to reduce the depth of the marking graph while the purpose of the partial order reduction techniques is to reduce its breadth. In a second part, we show by exploiting characteristic features of Petri nets, how we can take advantage of the strengths of each method and present a new technique namely persistent step sets as a parametric combination of the both methods leading to a state space that may be exponentially smaller than the full state graph, while preserving many behavioural properties of interest.

The verification of distributed algorithms is a challenge for formal techniques supported by tools, as model checkers and proof assistants. The difficulties, even for powerful tools, lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algorithms. Verification by construction can be achieved by using a formal framework in which models are constructed at different levels of abstraction; each level of abstraction is refined by the one below, and this refinement relationships is documented by an abstraction relation namely a gluing invariant. The highest levels of abstraction are used to express the required behavior in terms of the problem domain and the lowest level of abstraction corresponds to an implementation from which an efficient implementation can be derived automatically. In this talk, we will show a methodology based on the general concept of refinement and used for developing distributed algorithms satisfying a given list of safety and liveness properties. The modelling methodology is defined in the Event-B modelling language using the IDE RODIN. More precisely, we show how Event-B models can be developed for specific problems and how they can be simply reused by controlling the composition of state-based models through the refinement relationship. Following Polya, we have identified patterns expressed as Event-B models which can be replayed for developing distributed algorithms from requirements. Consequently, we obtain a (re)development of correct-by-construction existing distributed algorithms and a framework for deriving new distributed algorithms (by integrating models) and for ensuring the correctness of resulting distributed algorithms by construction. We illustrate our methodology using classical problems as communication in a network, leader election protocol, selfstabilisation. These works have been carried out in collaboration with partners of the ANR project RIMEL which have considered as well the local computation model defining distributed computations as graph rewriting rules (see http://visidia.labri.fr ). We will show how the local computation model can be used within the EventB framework. Resources are available at the link http://eb2all.loria.fr and are part of the current project on developing an atlas of correct-byconstruction distributed algorithms.

Distributed algorithms are designed for distributed systems. They aim to make nodes collaborate to achieve common tasks and/or solve global problems. A distributed system is represented by a simple connected graph where vertices correspond to processes and edges to direct communication links. Each process in the system represents an entity that is capable of performing computation steps, sending messages via some ports and receiving any message via some port that was sent by the corresponding neighbour. We consider asynchronous systems, i.e., each computation may take an unpredictable (but finite) amount of time. Nodes are also considered as anonymous: unique identities are not available to distinguish the processes (or we cannot guarantee that they are distinct). In this model, a distributed algorithm is given by a local algorithm that all processes should execute; thus the processes having the same degree have the same algorithm. A local algorithm consists of a sequence of computation steps interspersed with instructions to send and to receive messages. A probabilistic algorithm is an algorithm which makes some random choices based on some given probability distributions; non-probabilistic algorithms are called deterministic. A distributed probabilistic algorithm is a collection of local probabilistic algorithms. Since our systems are anonymous, if two processes have the same degree their local probabilistic algorithms are identical and have the same probability distribution. Designing probabilistic algorithms can be easy. However, analysis of such algorithms is very challenging. In this talk, we will introduce concentration inequalities that can be used to analyse such algorithms. The goal is to obtain lower and/or upper bounds on their time complexity.