Official course description, subject to change:
Basic info last published 14/10-21

Program Verification, MSc

Course info
Language:
English
ECTS points:
7.5
Course code:
KSPRVER1KU
Participants max:
12
Offered to guest students:
yes
Offered to exchange students:
yes
Offered as a single subject:
yes
Price (single subject):
10625 DKK
Programme
Level:
MSc. Master
Programme:
MSc in Computer Science
Staff
Course manager
Associate Professor
Teacher
Assistant Professor
Course semester
Semester
Forår 2022
Start
31 January 2022
End
27 May 2022
Exam
Abstract
> “Program testing can be used to show the presence of bugs, but never to show their absence!” > > ― Edsger W. Dijkstra (1970) Computer programs are ubiquitous in modern-day society. Software controls a wide variety of systems ranging from the mundane (children's toys, fridge timers, ...) to every-day and work-related items (computers, phones, laptops, ...) to safety-critical systems (cars, medical equipment, avionics, ...). While we may not care too much if a toy malfunctions or if our laptops do something unexpected we are far less likely to accept if the anti-lock breaks of a car stop working (Toyota Prius recall in 2013-2015), if a fighter-jet crashes due to bugs in the steering software (JAS 39 Griffin in 1989 and 1993), if a rocket explodes during take-off (Ariane 5 in 1996), or if a radiation therapy machine lethally irradiates patients (Therac-25 in 1985-1987). This course teaches program verification and formal methods -- how to prove, using computer-assisted logics and mathematics, that a program follows its specification to the letter without resorting to tests that never cover all possible edge cases of program execution. While this course does require a genuine interest in mathematics, you will not be doing proofs on paper but rather using the state-of-the-art interactive proof assistants Coq and SPARK. Both of these tools allow users to write programs and their specifications and to have them interactively checked by a computer and thus not only diminishing the possibility of human error, but they also providing users with a solid development environment, similar to an IDEs for standard programming languages, where proofs and programs can be developed, checked, and maintained, side by side. This course is also relevant for mathematicians who want to guarantee that their pen-and-paper proofs are actually correct by having them checked by a computer.
Description
This course teaches how to formally verify programs using the interactive proof assistants Coq and SPARK. These tools allow computer-aided support for writing proofs which is not only fun and highly addictive, but also help with the creative process as bugs in the proofs are quickly found by the tools, similarly to compilation errors of regular programs. While paper proofs frequently contain bugs, typos, and mistakes, machine-checked proofs typically do not. More precisely, the course covers the following areas. ### Coq * Writing programs in Gallina (the functional specification language embedded in Coq), * Code extraction * Intuitionistic logic * The Curry-Howard correspondence (proofs are programs) * Model-driven development * Program verification * Interactive theorem proving ### SPARK * Willard will write stuff here
Formal prerequisites
### Required * Discrete Mathematics * Introductory programming ### Recommended * 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:

Ordinary exam
Exam type:
Z. To be decided