Application-oriented Formal Verification Research Group at the Institute of Information Security and Dependability (KASTEL)
The Application-oriented Formal Verification research group is led by Prof. Bernhard Beckert and exists since 2009 at the Institute of Theoretical Informatics (ITI) and the KIT Department of Informatics. Since 2021, we are affiliated with the Institute of Information Security and Dependability (KASTEL), and we are still associated with the ITI.
Our main research topic is the practical application of logic and formal methods for the specification and verification of software. In particular, we address the following application areas:
- verification of functional properties and software dependability
- verification of relational properties and software evolution
- verification of information-flow properties and IT security
- verification of social choice algorithms and voting rules
News
Modern safety-critical systems consist of components in different programming languages and paradigms. Our PLDI paper introduces Heterogeneous Dynamic Logic (HDL), which allows us to combine proof calculi from distinct program logics in a modular fashion, much like SMT combines first-order theories. We demonstrate this on an automotive system where a Java controller steers a physical plant modeled in differential dynamic logic.
Our paper "Slicing Models for Equiconsistency with Alloy" was accepted at the International Conference on Rigorous State-Based Methods (ABZ 2026). It presents an application of SAT-based formal verification to a challenge in model-driven engineering. The paper proposes a novel method for extracting minimal model slices that preserve cross-domain consistency. The approach formulates slicing as a synthesis problem and solves it using counterexample-guided inductive synthesis (CEGIS), implemented in Alloy. This reduces model size while preserving the information required for consistency analysis in heterogeneous model-driven development.