Foundations of Certified Programming Language and Compiler Design

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.

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 Coq and Lean. 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.