Abstract

The Internet of Things (IoT) promises to improve people's everyday lives but the close interaction with Humans imposes stringent constraints on software. Smart factories, smart medical devices and autonomously driving cars are among the most prominent use cases where software interfaces with people closer than ever before. So close that in many IoT use cases, software takes control even in critical situations. When this happens, a faulty software puts lives at risk. More than ever, we need strong guarantees that the IoT software is correct.

From the last decades, we have learned that developing correct programs is nearly impossible and our approaches to detecting the problems (bugs) is flawed. The advances in heterogeneous processor architectures that span even into the cloud data centers made it nearly impossible to develop correct programs even for experts. The prevalent programming languages such as Java, C/C++, etc. offer almost no help to tame this complexity and guarantee a bug-free execution. So far, performance optimizations were the dominating incentives of a compiler. Consequently, testing sets out to hunt the bugs in a program. But testing is not only limited by its design but also extremely energy-consuming and still lacks automation. After all finding good tests is hard and now often augmented by machine learning. The more complex the software is the harder it gets to find good tests and the more (machine) learning and test execution is required.

In this lecture, we study the foundations of formal verification. In formal verification, the compiler is augmented with a theorem prover that assists the programmer to develop mathematical proofs for important properties of the program. We give an introduction to formally verified software development with special focus on programming language and compiler construction. The lecture is split into two parts.
The first part of the lecture introduces the deep connections between logic and type systems that are required to prove programs correct. The second part applies these techniques to the construction of a simple language and its compiler to prove properties such as semantic preservation and determinism.

By the end of the course, the students will understand the connections between a proof and a proposition in relation to a program and its types. The students will be able to develop programs and proofs both in Haskell and Coq. Furthermore, the course teaches different representations of programming language semantics that underpin the verification technique for programming languages, compilers and even processors for the various IoT scenarios ranging from small medical devices to programming in the cloud.

Lectures and exercises: 

The module includes a lecture (2 SWS) and an exercise (2 SWS) per week.

Prerequistes: 

Undergraduate courses in programming ("Programmierung") and logic ("Logik").

Module numbers: 

INF-DSE-20-E-FCPLCD

NES-INF-E-FCPL

Lecturer and responsible chair at TUD: