Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Research

Research

Research Interests

The vision of our team is the computer-aided construction of concurrent systems. Our ambition is to provide tool support for the full design space, from high-level programming languages down to assembly code, and from message passing concurrency to shared address spaces. To achieve this, our ambition is to understand the principles underlying concurrent computation and exploit them in the development of efficient verification and synthesis algorithms. Methodologically, we focus on three system classes placed at different levels in the design space: assembly programs executed on high-end processors, lock-free data structures invoked by programming-language threads, and functional programs placed in a reactive environment.

The classes come with different characteristics that suggest distinct (algorithmic) analysis problems. In assembly-level programs, we experience the influence of the hardware architecture on the program semantics. Our research serves as a stepping stone beyond verification towards automatic correction as needed during compilation and porting efforts. In lock-free data structures, the challenge is to take into account the memory management, and our goal is to optimize the allocation and reclamation behavior. Functional programs do not experience side effects, the only interaction with the environment is via method calls and returns. Our goal is to synthesize parts of the application from language-theoretic specifications.

Our research employs techniques from various branches of theoretical computer science. Automata and games provide elegant representations for the operational behavior of programs. Arguments on the program semantics justify these representations. Computability results help us evaluate the expressiveness of program classes and the hardness (decidability and complexity) of analysis problems. While these judgements provide worst-case bounds, industrial examples exhibit regularities that state space exploration techniques from computer-aided verification exploit to reduce the analysis effort.

Topics

Please follow the links to learn more about the group members working on a topic, the related publications, and the funding.

Projects

Past Projects