Formal Reasoning about Software

In this course, we learn the fundamentals of formal reasoning about programs. The basis for reasoning is logic, specifically, propositional and predicate logic. Within logic, we formally specify programming languages, that is, their syntax and operational semantics. We also formulate specifications of programs and prove that given programs satisfy their specification. The logic we work in is itself implemented as a computer program, in a so-called computer proof assistant. We learn how to implement our logical reasoning in a computer proof assistant; the activity of "proving" thus becomes a form of programming itself.

The final grade of the course consists of the following components:

• Individual Report (weighting 100%)

Final grade calculation = 1 * Individual Report

A passing final grade for the course can only be earned when for all components at least a 5.0 is earned, and the weighted final grade is at least a 5.8.

In case of an insufficient final result, repair options may exist in accordance with Article 17A, Times and number of examinations, sub 1, of the Teaching and Examination Regulations, for:

• Individual Report: Repair opportunity

Disclaimer: information may change depending on unforeseen circumstances or measures (see: TER Art 2, sub 5).