LARA

This is an old revision of the document!


Formal Verification EPFL Course (CS-550), Fall 2019

Moodle

Autumn 2019 Semester. 2h Lectures, 2h Exercises, 2h Labs. Continuous Control

Formal verification finds proofs that computer systems work under all scenarios of interest. Formal verification tools help developers construct such proofs, automatically searching for proofs using theorem proving and constraint solving (using, e.g. SMT solvers), and static analysis to discover program invariants. When it succeeds, formal verification is guaranteed to identify all software errors, including, for example, security vulnerabilities or cases when the computation produces a wrong numerical or symbolic result. The best approach to obtain formally verified software is to perform formal verification while software is developed, as opposed to after the fact.

Warmup videos by others: