Program Verification, BSc
AbstractThis is a hands-on course that teaches you how to prove that programs are correct. You will get in-depth experience with tools for this task, as well as an understanding of the theory behind them. This course thus equips you to pursue a career in writing safety-critical systems, or in pursuing higher studies in this area.
“Program testing can be used to show the presence of bugs, but never to show their absence!” ― Edsger W. Dijkstra (1970)The predominant method developers use to ensure that software behaves as intended, is testing. However, no amount of testing can guarantee the absence of errors. While errors in business applications are often tolerated, the same cannot be said for software found in medical equipment, or for software used by aerospace and automotive industries. In such safety-critical systems, errors lead to significant monetary losses, destroyed equipment, even loss of life.
In this course you learn how to write specifications of programs and prove, using state-of-the-art tools, that these programs follow their specification to the letter. You will write proofs in a similar way to how you write programs, and you will use interactive and automated proof assistants to check that all of your proofs are correct. Having a computer check your proofs in this way
- significantly reduces the possibility of developer error, thus greatly improving the reliability of your software
- enables you to update proofs of correctness in a similar iterative manner as you write programs---a sharp contrast to the error-prone task of maintaining and checking paper proofs.
This course is relevant for anyone with an interest in program correctness, as well as for mathematicians with an interest in ensuring that their pen-and-paper proofs are correct by having them checked by a computer.
You will predominately be working with two tools in this course -- Coq and Spark.
Coq is an industry-grade interactive proof assistant that allows users to:
- write and prove mathematical theorems
- write programs and specifications in an embedded functional language called Gallina, prove properties about these programs, compile them to executable code, and run the verified programs
- step through proofs one line at a time, similarly to a debugger, in order to modify and develop the proofs as you go along.
SPARK is an industry-grade programming language for writing safety-critical systems, used by Boeing, Airbus, Lockheed-Martin, Toyota, NVIDIA, and others. SPARK allows you to
- write programs that compile and run, and write specifications for these programs.
- prove that a program satisfies its specification using third-party automatic or interactive theorem provers.
Tying it all together
Coq is very expressive allowing you to reason about a wide variety of programs and theorems; Spark has support for a wide variety of interactive and automatic proof assistants giving you a lot of freedom in how you approach your verification tasks.
- Discrete Mathematics
- Introductory programming
- Functional programming (it is perfectly fine to read both courses in parallel)
- Algorithms and data structures
Intended learning outcomes
After the course, the student should be able to:
- Characterise recent developments in programming languages and verification technology
- Create programs and their specifications using Coq and Spark
- Construct interactive proofs that show that programs follow their specifications
- Compare models of programs with their real-life counterparts
- Assess accuracy of models and make precise what impact any imprecisions have on any proofs made
- Apply and reflect on theories for modelling, analyzing and constructing programs, specifications, and their proofs of correctness
- Relate automated and interactive proof assistants and make precise the advantages and disadvantages of both types of systems
Ordinary examExam type:
D: Submission of written work with following oral, External (7-point scale)
D2G: Submission for groups with following oral exam supplemented by the submission. Shared responsibility for the report.