Research InterestsThe vision of our team is the computer-aided construction of concurrent systems on all design levels. To achieve this, our ambition is to understand the principles underlying concurrent computations and exploit them in the design of efficient algorithms. Methodologically, we focus on two system classes, multi-threaded software executed on high-end processors and reconfigurable systems present as internet applications and remote programs. We tackle disjoint problems in both classes. For reconfigurable systems, we investigate inference algorithms for qualitative properties. Our research on multi-threaded programs serves as a stepping stone beyond verification towards quantitative analysis, system correction, and ultimately optimisation.
Our research employs techniques from various branches of theoretical computer science. For reconfigurable systems, computability results on the decidability and complexity of verification problems help evaluating the expressiveness of system classes and the hardness of their analysis. While these judgements provide worst-case bounds, industrial examples exhibit regularities that state space exploration techniques from computer-aided verification exploit to reduce analysis efforts. Quantitative properties like the availability of network nodes raise problems of fundamental character in formal language theory. We strive for suitable automata models with appropriate closure properties, and search for their algebraic as well as logical counterparts.
Please follow the links to learn more about the group members working on a topic, the related publications, and the funding.
- Imperfect and Timed Systems
- Language-Theoretic Verification
- Monoids as Storage Mechanisms
- Relaxed Memory Models
- Theoretical Aspects of Verification
- Member of TUBS.digital.
- ArchiV: Architecture-Aware Verification. Carl Zeiss.
- Supported by the Competence Center High Performance Computing. Fraunhofer ITWM.
- R2M2: Robustness against Relaxed Memory Models. DFG.
- ROIS: Robustness under Realistic Instruction Sets. DAAD-PROCOPE.
- PAMS: Parallel algorithms for multiscale simulations. Center for Mathematical and Computational Modelling (CM)2.
- Transregional Research Center AVACS: Automatic Verification and Analysis of Complex Systems. DFG SFB.
- AVeriSS: Automated Verification of Software Systems. ANR.
- TrustSoft: Trustworthy Software Systems. DFG GK.