This repository is the homepage of the course Formal Verification and hosts the material necessary for the labs.
- Professor: Viktor Kunčak
The grade is based on the labs, written midterm exam, as well as code, documentation, and explanation of projects during the semester. Specific percentages will be communicated in the first class and posted here. Passing the course may require examinations throughout the semester.
In this course, we introduce formal verification as a principled approach for developing systems that do what they are expected to.
The course has two aspects:
- learning the practice of formal verification - how to use tools to construct verified software
- understanding the principles behind formal verification and the ways in which verification tools work
- [CalComp] The Calculus of Computation - Decision Procedures with Applications to Verification, 2007, from Springer, from EPFL library, by Aaron Bradley and Zohar Manna.
- [HandMC] Handbook of Model Checking, 2018, from from Springer, from EPFL Library, edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem.
- [HandAR] Handbook of Practical Logic and Automated Reasoning, 2009, from Cambridge University Press and from EPFL Library, by John Harrison
To see the material from last years, which may be more or less relevant, please visit https://mediaspace.epfl.ch , log in with your EPFL credentials and select this channel. Slides and listings are attached underneath the videos.