formal methods and tools

Nasty errors typically arise from interactions between concurrent subsystems. Therefore, concurrency theory is a fundamental background for our research and teaching. Central themes are process algebra, (timed/hybrid) automata, and temporal logic. We develop quantitative methods to analyse timing, reliability, and energy usage. We build ingenious tools for software analysis, based on automated reasoning, search algorithms, and multi-core techniques.

Example applications are the verification of the java.util.concurrent library and the analysis of railway safety systems.

Chat offline (info)