Formal Methods
"Formal Methods" develops methodologies, algorithms, and tools for the rigorous specification, design, verification, and testing of software-intensive systems. We conduct research on theorem proving, state-space exploration techniques - in particular model-checking - abstract interpretation and testing. We also study and contribute to the scientific foundations of these techniques, including automata theory, formal semantics, computational logic, concurrency theory, game theory, computer algebra, and algorithms and data structures.
Current research areas include the development of: verification techniques for stochastic and hybrid systems, game-theoretic techniques for automatic synthesis, verification software that is itself formally verified, program analysis tools for complex high-level software, and software engineering solutions to software and data security. Our results and tools find application in several areas, including automotive and avionics software, power grids, autonomous cars, and robotic systems.
Jan Kretinsky, Prof. Dr. rer. nat.
Harald Räcke, Prof. Dr.
Exemplary projects
The DFG Research Training Group ConVeY studies the design and analysis of cyber-physical systems, that is, software controlled systems that interact with the physical world and have to deal with the continuous nature of physics.
The goal of this project is to verify the mathematical foundations for the quantitative analysis of algorithms using the Isabelle theorem prover, and produce a library of efficient deterministic and randomized algorithms for which both correctness and runtime have been mechanically verified.
The goal of the project is to develop methods for a faster and more efficient development process of safety- or operation-critical cyber-physical systems in (partially) unknown environments, for which we synthesize and verify controllers on-the-fly during system execution. This requires the unification of control and verification approaches, which were previously treated separately by developers.