Verified Algorithms
Verified algorithms are algorithms that come with a computer-checked guarantee that they perform what is specified. This course teaches how to obtain such algorithms using a proof assistant named Coq.
Verified algorithms are crucial for domains where the presence of bugs are unacceptable for society: computer security, financial transactions, transportation embedded software, computer infrastructure.
Outline of the course
- Programming with simple types and recursive data-type course notes, predefined functions for the exercises, examples used in the course
- Expressing requirements with logical formulas and advanced types, course notes
- Tactic-based theorem proving
- Reasoning by induction on programs, course notes, diagnostic questions, answers, quick reference
- Verified algorithms in data processing, course notes, examples
- Verified algorithms in number processing
- Verified compilation
The various techniques used in this course will be illustrated during lab sessions using the Coq system (ACM software system award 2014). A downgraded version can be used for experimenting at this address.
References
- Coq’Art.
- Software Foundations.
- Example of a program that was verified in Coq : Sudoku.
- Example of a program where parts are verified in Coq : trajectory computation .
- Git repository for the course : https://gitlab.inria.fr/bertot/verified-algorithms-25
