Recurrence Sets for Proving Fair Non-Termination under Axiomatic Memory Consistency Models has been conditionally accepted.
Oriented Metrics for Bottom-Up Enumerative Synthesis has been conditionally accepted.
Dartagnan won silver and gold medals at SV-COMP2025. It won silver as verifier and gold as validator in the ConcurrencySafety category.
SNIP: Speculative Execution and Non-Interference Preservation has been accepted.
DOI
to the webpages of the Institute of Theoretical Computer Science. The vision of our team is the computer-aided construction of concurrent systems, on all levels in the design space. To this end, our ambition is to understand the principles underlying concurrent computation and exploit them in the development of efficient verification and synthesis algorithms. Harnessing methods from automata theory, games, semantics, and computer-aided verification the institute is specialized in inference techniques for qualitative as well as quantitative properties, and currently extends verification algorithms towards automatic system correction, optimization, and synthesis.
Further Information
To get an impression of our research topics and courses, consider
If you would like to join us, if you are interested in a Bachelor's, Master's, or PhD thesis, or in case you are just curious about who we are - we warmly welcome you to visit us. We offer beautiful topics, interesting projects, competitive positions, and an international research environment.