Formal Methods at Work
The main aim of this ten-hour course is to give you hands-on 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 real-time systems. (The prime
architects behind Uppaal have received the
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
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!
A First Introduction to Uppaal.
In J. Tretmans, editor.
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 real-time.)
- 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
If you want to see a proof of the fact that solving the gossiping-girls problem requires 2n-4 calls when the number of girls is n>=4, see the paper
of the talk Formal Reasoning about the Security of Amazon Web
Services by Byron Cook (Amazon Web Services and University
Video of the
talk Continuous Reasoning: Scaling the impact of formal
methods by Peter O'Hearn (Facebook and University College
- Video of a LogicLounge with Dana S. Scott.
- Watch the recordings of the talks at the recent
and Verification Symposium (FaceTav 2017).
Synthesis and Optimization for Cyber-Physical Systems, invited
talk by Kim G. Larsen at ETAPS 2017 in Uppsala, sweden.
- The seL4 Microkernel, the
world's first operating-system kernel with an end-to-end proof of
implementation correctness and security enforcement. You can read the
Verified Software Kernels: Raising the Bar for High Assurance
- 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
Fast with Software Verification. Proceedings of the NASA Formal
Methods - 7th International Symposium: 3-11, 2015.
Code Confirmed" by Kevin Hartnett, Quanta Magazine, September 20,
- Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc
Amazon Web Services Uses Formal Methods. Communications of the
ACM, Vol. 58 No. 4, Pages 66-73.
- Galois Inc. Blog: Posts on Verifying Amazon's s2n HMAC with SAW.
- Facebook Infer.
RacerD: Fast static race detection at scale by Sam Blackshear and
C.A.J. Hurkens. Spreading
gossip efficiently. Nieuw Archief voor Wiskunde,
5/1(2):208-210. June 2000.
More problems will be added in due course, also depending on how quick
you are at solving them.
- How much can we lose?
much can we reach?
- Model the one- and two-dimensional solitaire games described
using Uppaal, check that the game can indeed be solved and find the
- Modelling of classic and real-time 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.
The project for the course is described in
this PDF file.