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
This paper presents RAG4C, an observable-centric framework for checking semantic consistency across requirements and models in multidisciplinary model-driven development. It uses retrieval-augmented generation, LLMs, and ontology construction to extract shared domain properties and translate their constraints into solver-ready formulas. By aligning heterogeneous terminology and detecting contradictory constraints early, RAG4C reduces manual consistency-checking effort and supports more reliable development. The evaluation of synthetic and industrial automotive requirements demonstrates high accuracy and scalability.
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.
Prevailing program verification approaches tend to evolve in isolation, building on expressive and powerful formalisation and modelling concepts that lack compatibility with other techniques. In our FM paper, we introduce a framework that enables different deductive verification techniques to cooperate when reasoning about encapsulated data structures. By using algebraic data types as a common semantic foundation, the approach allows to verify a Java project cooperatively between VeriFast (Separation Logic), KeY (Dynamic Frames), and Universe Types (a flavor of Ownership Types).
Our paper introduces a formal way to treat analyses as first-class elements in model-driven development. It shows how analysis results and their dependencies can be represented explicitly, so that only affected analyses need to be re-executed after model changes. This supports incremental recertification and helps make consistency management for cyber-physical systems more efficient.