Formal Methods at Work
GSSI, November
2018
Welcome
The main aim of this tenhour course is to give you handson experience in applying formal methods to the modelling and analysis of problems.
During the course, I plan to do very little lecturing. Since
what we learn we learn by doing, during most of the course sessions,
you will be working in groups of two on modelling and
analysis problems using the model checker
UPPAAL, which is the foremost tool
suite for the automatic verification of realtime systems. (The prime
architects behind Uppaal have received the
CAV Award
2013.
Each group can solve the given problems at its own speed. At
the end of the course, each group will deliver a report describing its
solution to the problem posed in the project description presented
below.
At the end of the day, I hope that you will have a lot of fun
in working on these problems and using Uppaal to solve them!
Recommended literature

F.W. Vaandrager
A First Introduction to Uppaal.
In J. Tretmans, editor.
Quasimodo Handbook.
To appear, 2014. (The link also points to files with the models mentioned in the book chapter.)

Gerd Behrmann, Alexandre David and Kim
G. Larsen. A
Tutorial on UPPAAL.
 Introduction to timed
automata and their basic theory (Slides). (Note: We will only cover the very basic notions of the theory presented in those slides that you will need to work on the problems having to do with realtime.)
 Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis and
Danny Boegsted Poulsen. Uppaal SMC
Tutorial. To appear in the journal Software Tools for Technology
Transfer. This is a tutorial paper devoted to the statistical model
checker that is now part of the Uppaal tool suite.
Other recommended resources

Video
of the talk Formal Reasoning about the Security of Amazon Web
Services by Byron Cook (Amazon Web Services and University
College London).

Video of the
talk Continuous Reasoning: Scaling the impact of formal
methods by Peter O'Hearn (Facebook and University College
London).
 Video of a LogicLounge with Dana S. Scott.
 Watch the recordings of the talks at the recent
Facebook Testing
and Verification Symposium (FaceTav 2017).
 Validation,
Synthesis and Optimization for CyberPhysical Systems, invited
talk by Kim G. Larsen at ETAPS 2017 in Uppsala, sweden.
 The seL4 Microkernel, the
world's first operatingsystem kernel with an endtoend proof of
implementation correctness and security enforcement. You can read the
white paper
Mathematically
Verified Software Kernels: Raising the Bar for High Assurance
Implementations.
 The CompCert project web
page. CompCert is a formally verified optimizing compiler for a
large subset of the C99 programming language. The compiler is
specified, programmed and proved in
Coq. It aims to be used
for programming embedded systems requiring reliability.
 Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi,
Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene
Papakonstantinou, Jim Purbrick, Dulma
Rodriguez. Moving
Fast with Software Verification. Proceedings of the NASA Formal
Methods  7th International Symposium: 311, 2015.

"HackerProof
Code Confirmed" by Kevin Hartnett, Quanta Magazine, September 20,
2016.
 Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc
Brooker, Michael
Deardeuff. How
Amazon Web Services Uses Formal Methods. Communications of the
ACM, Vol. 58 No. 4, Pages 6673.
 Galois Inc. Blog: Posts on Verifying Amazon's s2n HMAC with SAW.
 Facebook Infer.

Opensourcing
RacerD: Fast static race detection at scale by Sam Blackshear and
Peter O'Hearn.
If you want to see a proof of the fact that solving the gossipinggirls problem requires 2n4 calls when the number of girls is n>=4, see the paper
C.A.J. Hurkens. Spreading
gossip efficiently. Nieuw Archief voor Wiskunde,
5/1(2):208210. June 2000.
Problems
More problems will be added in due course, also depending on how quick
you are at solving them.
 How much can we lose?

How
much can we reach?
 Model the one and twodimensional solitaire games described
here
using Uppaal, check that the game can indeed be solved and find the
shortest solution.
 Modelling of classic and realtime mutual exclusion algorithms.
 Coffee machine.

The Little Book of
Semaphores by Allen B. Downey is a treasure trove of modelling and
verification exercises you might want to try. I will point out some
interesting ones to those who might be interested.
Project
The project for the course is described in
this PDF file.