The goal of formal methods in software engineering is to provide techniques for developing highly reliable as well as security critical software. Two steps are required to achieve this goal: An unambiguous specification of the system requirements and a mathematical proof (verification) that the implementation adheres to this specification.
Formal methods provide a wide variety of mathematically precise specification languages, such as higher order logic, algebraic specifications, abstract state machines, the Z notation, and temporal logic. These languages enable the unambiguous description of a system's expected behavior, thereby forming the basis of the later verification of the system's correctness. System correctness consists of different aspects ranging from functional correctness over safety and security to reliability.
Mathematical proofs of system correctness can be constructed using several approaches, such as interactive theorem proving, static code analysis, model checking, and SMT solving.
An important concept to handle complexity is refinement, which allows a modular, step-wise, top-down development of a system starting with an abstract formal specification, ending with verified code.
We are actively working on new techniques for formal system development. Our research focuses on refinement in combination with abstract state machines and temporal logic. Our group is developing the KIV System, an interactive theorem prover. We apply these techniques in practical applications, such as in our research projects VeriCAS (correctness of lock-free algorithms) and Flashix (development of a verified file system for flash memory).
We are offering our students lectures, lab courses, and seminars on formal methods and their application in the software engineering process.

1. Proving the functional correctness of safety- and security-critical systems

2. Consulting/training in the use of formal methods for the certification of software that meets the highest safety and security standards (e.g., SIL, Common Criteria)