The research groups semantics and verification of parallel systems was founded in 2019 and has benn led by Prof. Dr. Marie-Christine Jakobs until she moved to LMU Munich in April 2023.
The goal of software verification is to check whether a program satisfies certain properties. Properties of interest are many-fold and range from the absence of runtime errors (division by zero, null pointer dereference, etc.) over termination to functional properties like a programs sorts the input list.
Software verification plays an important role for today’s society. Software systems are all around us. While a crash of our cellphone caused by a software error is annoying, a software error in safety-critical applications like automatic cruise control can be catastrophic.
To check properties of a program, we need to know the semantics of the program, i.e., a description of the possible executions of a program.