Program Verification
- Jesper Bengtson Course manager
-
Willard Rafnsson
Teacher
This hands-on course teaches you how to prove that programs are correct. Rather than testing a program on selected inputs, you learn to specify what it should do and to establish, with machine-checked proof, that it does so for all inputs. This is the basis for building safety-critical and security-critical systems, and for pursuing further studies in formal methods.
You work predominantly with two industry-grade verification tools, the Coq proof assistant and the Frama-C analysis framework, and the course culminates in a one-month project. The course is demanding and has a strong emphasis on logic and mathematics.
About the course
The course is part of both the Security and the Software Analysis specialisations of the MSc in Computer Science at the IT University of Copenhagen (7.5 ECTS, taught in spring). It is also offered as a PhD course.
Learning objectives
After taking this course, students will be able to:
- formally specify the intended behaviour of programs
- prove programs correct using logic-based techniques
- use Coq and Frama-C to mechanise specifications and proofs
- apply verification to safety-critical and security-critical code
Topics
- Program specifications and program logics
- Interactive theorem proving in Coq
- Deductive verification of C programs with Frama-C
- Reasoning about correctness of safety-critical software
- Verification project