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
- EDS @ SYN: Effective Denotational Semantics for Synthesis. DFG.
- Virtual Test Analyzer. IAV.
- Humboldt Research Award for Ahmed Bouajjani, with Javier @ TUM and Viktor @ MPI-SWS.
- ArchiV: Architecture-Aware Verification. Carl Zeiss.
- R2M2: Robustness against Relaxed Memory Models. DFG.
- Supported by the Competence Center High Performance Computing. Fraunhofer ITWM.
- ROIS: Robustness under Realistic Instruction Sets. DAAD-PROCOPE.
- PAMS: Parallel algorithms for multiscale simulations. (CM)2.
- AVeriSS: Automated Verification of Software Systems. ANR.
- AVACS: Automatic Verification and Analysis of Complex Systems. DFG SFB.
- TrustSoft: Trustworthy Software Systems. DFG GK.