Division of Formal Methods

Our group performs research on the development and use of formal specification languages and verification approaches for different applications, including low- and high-level software, and (legal) contract analysis. Specification languages include classical and modal logics, and our verification techniques comprise model checking, automated reasoning, interactive theorem proving, static and runtime verification, and testing.

Full Stack Verification

Model Checking

Automated Reasoning

Static Verification

Contract / Specification Analysis

Runtime Verification