Advanced Verification and Validation (AVV)
Do you know why the French are so good at playing football and building reliable software? Well, the football is just luck, but French scientists have now revealed the secret to reliable software: machine reasoning.
In this course, we will explore machine reasoning techniques, from computational logic to abstract interpretation, that go beyond simple testing and provide strong guarantees about the behavior of software systems. Then, you will build software as reliable as Airbus aircraft!
- Lectures / Labs:
Tuesdays 12:15, Δ-1026 (Cours Magistral).- Wednedays 14:00, Δ-3022 (Consultations).
- Thursday 12:15, Δ-1022 (Travail Dirigé).
- Textbooks:
- Samuel Mimram, "PROGRAM = PROOF", École Polytechnique, 2020.
- Patrick Cousot, "Principles of Abstract Interpretation ", MIT Press, 2021.
- Xavier Rival and Kwangkeun Yi, "Introduction to Static Analysis", MIT Press, 2020.
- Instructor(s):
Course Plan
The grading in the course will be based on your project. The project can be done in teams or individually. The project has to be open source and contributions must be made under your real account on github, bitbucket, etc. In terms of content, there are two kinds of admissible projects.
- You may apply advanced verification techniques to solve a verification challenge.
- You may contribute to the development of advanced verification techniques.
Advanced verification techniques are the techniques covered in this course. If you do not have your own verification challenge or pet static analyzer to work on, you can contribute to the Goblint static analyzer.
In order to prepare you for the project, we will work through Samuel Mimram's course on Computational Logic and the LIP6 course on Abstract Interpretation. We will solve these exercises together, but those interested in learning OCaml and Agda are strongly advised to solve at least some of the exercises on their own before we discuss them. While your grade depends on the project, advanced verification tools tend to be written in OCaml, so it is important to pick it up if you want master these techniques.
Grading and requirements
The project is graded according to the following (almost) three-valued logic. I will describe it for project that contribute to the Goblint analyzer, but the same principle applies if you submit your work to, e.g., the archive of formal proofs or any other repository with rigorous peer review:
- If you don't do anything for the project, you will fail the course.
- If you submit a public pull request to the goblint repository, you will receive at least a B (unless it's very obviously a vacuous pull request).
- If your pull request is merged, you are guaranteed to receive an A.
- If your pull request is not merged, I will evaluate the quality of your pull request (code & documentation) as well as your interaction with the maintainers.
That's it. Surely, this is one of the easiest ways to receive good grade while doing something good in the world!