Program Verification, MSc (Spring 2022)

Abstract

This 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.

Description

“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.

You will also learn the theoretical underpinnings required to make these tools function, giving you a solid understanding of how programs and their proofs of correctness are connected.

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

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

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.

Automated proof assistants attempt to prove theorems automatically, similarly to how an IDE type checks your programs automatically. When they fail to do so, SPARK lets you use more generally-applicable interactive theorem provers (like Coq).

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.

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:

• 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.

Learning activities

• Weekly lectures
• Weekly exercises
• Project

Lectures present the background, theory, and methods needed for achieving the intended learning outcomes providing the theoretical underpinnings for the course curriculum.

Assignments give you the necessary practical experience required to achieve proficiency in the course material and to prepare you for the larger projects.

 The exercise sessions allow you to work on assignments and projects under supervision allowing for discussion and reflection of how to convert theory into practice.

The mini-project provides a simple program that you must prove correct and extract into executable code, using the knowledge procured in the assignments, and allows you to investigate and understand how software is verified from start to finish.

The mandatory project allows you to investigate in depth a part of the curriculum that appeals to you. Your choice of project is relatively free, but must be approved by the teachers.

Mandatory activities

• There will be seven weekly hand-in assignments, all of which you must pass before you start your project. An exact hand-in date will be given at the start of the course.
• One mini project spanning three weeks. An exact hand-in date will be given at the start of the course.

The student will receive the grade NA (not approved) at the ordinary exam, if the mandatory activities are not approved and the student will use an exam attempt.

Course literature

• Software Foundations Author: Benjamin Pierce https://docs.adacore.com/spark2014-docs/html/lrm/

Student Activity Budget

Estimated distribution of learning activities for the typical student

• Preparation for lectures and exercises: 10%
• Lectures: 17%
• Exercises: 17%
• Assignments: 30%
• Project work, supervision included: 20%
• Exam with preparation: 6%

Ordinary exam

Exam type:
D: Submission of written work with following oral, External (7-point scale)
Exam variation:
D2G: Submission for groups with following oral exam supplemented by the submission. Shared responsibility for the report.

Time and date