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

Specification and Analysis of Normative (Legal) Documents

Runtime Verification