ACF : Analyse et Conception Formelles

Subjects: functional programming, first order logic, formal specification and formal verification;
Tools: Isabelle/HOL 2023 (please use this version!) proof assistant and counter-example finders (see a short introduction) and the 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.

ACF on Moodle with forums etc. (Only for students from University of Rennes)
The course video channel (In french)

Isabelle/HOL solutions of exercises (uploaded after each lecture)

Subjects for lab sessions TP0, TP1, ... are is in the tab

Archive of ACF exams

Complete lecture notes, in one file

The Isabelle/HOL survival kit gives an idea of the used subset of Isabelle commands.

A detailed bibliography for Isabelle/HOL and Scala.

A complete course with videos on (OCaml) functional programming. This is not the same programming language but can be useful for begginers in functional programming. There is also a book on the same subject.

We use Isabelle/HOL 2023 (please use this version, if possible). See the installation instruction first! Then, if you plan to use Isabelle/HOL for all lab sessions, you will have to install and configure a few things:

To have a full quickcheck (with narrowing): install the Gnu Haskell Compiler and in the file $ISABELLE_HOME/etc/settings, set the ISABELLE_GHC variable to the path where the binaries of the compiler (i.e. the command ghc) is installed

Scala 2.13 and SBT (Scala Build Tool). Here are some explanation on how to use those tools on ISTIC computers and on your computer.
If your computer gets stuck while running Isabelle/HOL: By default Isabelle/HOL processes different part of your thy files in parallel. If you use Nitpick/Quicheck at different places in your file, they will all be called in separate threads. If your computer gets blocked because of that, you may limit the number of threads used by Isabelle/HOL.

In Isabelle/HOL menus: Plugins>Plugin option>Isabelle>General, in the "Parallel processing and Timing" section, for "Threads" replace the value 0 (which means no limits) by 2 (i.e. a maximum of two threads) or even 1 if your computer is not powerful enough.

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. Lectures contains exercises that are solved on Isabelle/HOL by students (available after the lecture). Here is the course schedule, click on one element for more details.

TP0 - Lab session: teasing!

Teasing... a simple Java lab session tp0.pdf (or Python lab session tp0_python.pdf)... to show that designing a (simple) software can be very error prone. It is nearly impossible to directly come up with the correct program for this (refined) simple list inclusion test, either in imperative or in recursive style. The objective is to motivate the fact that defining the expected properties is crucial to detect problems and, in the end, be sure that the solution is correct. An (opaque) Java oracle TP0_ACF.zip (or Python oracle TP0_ACF_Python.zip) is given to the students to test their code and know how far their program is from the solution. An overall of 5% students ended up with the correct program within 2 hours.

Lecture: Overall objectives and organization of the course.

intro.pdf. Video (in french).

CM1 - Lecture: Propositional and first order logic, interpretations and models in Isabelle/HOL (auto+nitpick).

cm1.pdf. Video (in french). Initial theory for the course cm1.thy.

CM2 - Lecture: Terms, functions, lambda-calculs and types (export_code to Scala).

cm2.pdf. Video (in french). Initial theory for the course cm2.thy.

TP1 - Lab session: propositional and first order logic in Isabelle/HOL (auto+nitpick).

tp1.pdf, initial theory for the lab session tp1.thy : first lab on Isabelle/HOL: propositional and first order logic (auto+nitpick). There are some additional exercises for those who wants to know more about proof techniques in Isabelle/HOL: tp1bis.thy.

CM3 - Lecture: Recursive functions (fun, function, primrec) and termination.

cm3.pdf. Video (in french). Initial theory for the course cm3.thy

CM4 - Lecture: basic proof tactics (auto, induct, sledgehammer, nitpick, quickcheck)

cm4.pdf. Video (in french). Initial theory for the course cm4.thy : basic proof tactics (auto, induct, sledgehammer, nitpick, quickcheck). The more advanced topics of this course are presented in this other video (in french) with the pc.thy Isabelle/HOL file. Students interested by a deeper presentation of the proof assistant can have a look to the Isabelle/HOL tutorial in the short Isabelle/HOL bibliography.

TP2 - Lab session: Recursive functions and basic proof tactics. Defining and proving usual boolean operations on sets implemented as lists.

tp2.pdf : Recursive functions and basic proof tactics. Defining and proving usual boolean operations on sets implemented as lists in this (empty) theory file (tp2.thy). We do the same for a basic implementation of tables (table.thy). We also provide an other exercise which is a simple theory file (tp3Bis.thy) in which the 4 main lemmas admit counterexamples. Some of the lemmas need some fine tuning of Nitpick and Quickcheck for the counterexamples to be found: this is the purpose of this exercise.

CM5 - Lecture: Scala Crash Course

cm5.pdf Scala Crash Course. Video (in french). We start from the following Scala source files. Basics of Scala, functional programming in Scala, object model, case classes, pattern-matching and interoperability with Java. Deeper informations on the language are available from M. Odersky, L. Spoon and B. Venners online book and from those selected documents.

TP4 - Lab session: Scala programming.

tp4.pdf Implementation of an evaluator and a pretty printer for a simple imperative language... using pattern matching to avoid using the visitor design pattern. We start from the following project (TP4_ACF.zip).

TP4bis - Lab session: Deciding equivalence of arithmetic expressions in Isabelle/HOL

tp4bis.pdf Deciding equivalence of arithmetic expressions. We start from the following Isabelle/HOL theories: tp4bis.thy and table.thy.

CM6 - Certified programming and existing certified programming chains

cm6.pdf. Video (in french). Initial theory for the course cm6.thy.

TP5 - Lab session: Deciding equivalence of firewall security policies

tp5.pdf, tp5.thy, TP5_ACF.zip Students have to define a predicate deciding the equivalence of security policies used by a firewall. A security policy (also known as a chain) consists of a list of rules which are applied using their priority, i.e. their order in the list. Maintaining such policies is a well-known difficult problem because any update in a policy (like a simple reordering of the rules) may totally change the security property enforced by the firewall. Having an equivalence predicate on policies permits to check (in a formally proven way) that an update of the security policy does not change the protection enforced by the firewall.

CM7 - Lecture: Software verification techniques

cm7.pdf. Video (in french). Initial theory for the course cm7.thy .

TP67 - Lab session: Designing a simple (yet proved) static analyzer

tp67.pdf, tp67.thy, TP67_ACF.zip : Students design a static analyser for a simple toy language, define the correctness theorem to guarantee the safety of the analyzer, define the completeness theorem to refine it (using the counterexamples). Integrated with a Scala parser for the toy language. Proofs are optional. To carry out the proofs, you can get inspiration from this short video (in french) with the pc.thy Isabelle/HOL file.

TP89-10 - Lab session: Designing a validation tool for a price negociation web application

tp8-10.pdf, tp8-10.thy, TP89_ACF.zip, table.thy: Students design a validation tool for a price negociation web application. A merchant and a client send messages to the validation tool to negociate a price. A price is validated if a price proposed by a client is superior or equal to a price proposed by the merchant. In the end, the list of validated should be correct. As with all protocols, more complex than it seems at first glance. They define the functions, check the 9 properties and export the Scala code. All the validations tools of all students are then deployed on a web site so that all students can attack all validation tools and report on the attacks found. Proofs are optional. To carry out the proofs, you can get inspiration from this short video (in french) with the pc.thy Isabelle/HOL file. For this lab session a list of relevant intermediate lemmas (in french) is also provided: tp8-10proof.thy

Instructor: Thomas Genet

Teaching assistants (2023-2024)

Thomas Anberrée, Benoît Montagu, Benjamin Farinier, Joseph Lallemand, and Stanislas Riou.

Past teaching assistants

Olivier Barais, Aurèle Barrière, Erwan Bousse , Benoît Combemalle, Khalil Ghorbal, Manuel Leduc, Vincent Rebiscoul, Julien Richard-Foy, Sophie Pinchinat , Ocan Sankur, 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.