ACF : Analyse et Conception Formelles

"Software Formal Analysis and Design"

First year of Master in Computer Science at ISTIC, Université de Rennes 1

Instructor: Thomas Genet

Teaching Assistants (2021-2022): Vincent Rebiscoul, Benoît Montagu and Ocan Sankur.

What is it about?

  • Subjects: functional programming, first order logic, formal specification and formal verification;

  • Tools:    Isabelle/HOL  Isabelle/HOL 2020 (and no other version) proof assistant and counter-example finders (see a short introduction) and the Scala programming language.

This course is about using formal methods to design verified software components. To tackle this goal we rely on functional programming, first order logic for specifying properties, proof assistant for property checking on programs and the Scala programming language for integrating the verified components into a Java application. With regards to verification, we study and use the powerful proof tactics and counter-example finders embedded in the Isabelle/HOL proof assistant. For code generation, we use the awesome Scala code exportation feature of Isabelle/HOL.

The students' final achievement is a verified Scala component achieving price negociation in a web application. The component is designed and verified in Isabelle/HOL. Then, the functional code is exported to Scala and integrated in the Java (web) application.

Disclaimer: this is a course on formal software design and not on proof design. Students are given a limited set of proof tactics that is enough to prove properties defined during the lab sessions. However, resulting proofs can be long and cumbersome. As a result, it is accepted that properties are not proven but only checked using Isabelle/HOL powerful counter-example finders.

Teaching material

The course consists of 7 lectures and 11 lab sessions. Lecture notes (cm1.pdf to cm7.pdf) are (almost) in english, the lab notes (tp0.pdf to tp8-10.pdf) are in french. The Isabelle/HOL survival kit gives an idea of the used subset of Isabelle commands. Lectures contains exercises that were solved on Isabelle/HOL by students on my computer (and projected) during the lecture. The course schedule is the following: 

Tools for Lab sessions

Past teaching assistants

Olivier Barais, Aurèle Barrière, Erwan Bousse , Benoît Combemalle, Khalil Ghorbal, Manuel Leduc, Julien Richard-Foy, Sophie Pinchinat , and Pierre Wilke


Many thanks to people of the Isabelle/HOL team at TUM: Tobias Nipkow, Jasmin Blanchette, Lukas Bulwahn, Florian Haftmann and Alexander Krauss for answering questions and for fruitful discussions.

Many thanks to
Olivier Barais, Sandrine Blazy, Benoît Combemale, Arnaud Jobin, Julien Richard-Foy and Gweltaz Riou for their help during the preparation of this course.