Welcome
to the webpages of the Institute of Theoretical Computer Science. Our team investigates the foundations of concurrent behaviour in network applications, remote programs, and multi-threaded software. Our ambition is to understand the underlying principles and exploit them in the design of highly efficient analysis algorithms. Harnessing
methods from computability theory, computer-aided verification, and formal languages, the institute is specialised in inference techniques for qualitative as well as quantitative properties, and currently extends state space exploration algorithms towards automatic system correction and optimisation.
Roland Meyer
Contact and Impressum
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, competitive scholarships, and an international research environment.
TACAS 2018
Fine-Grained Complexity of Safety Verification .
publications
FSTTCS 2017
Verification of Asynchronous Programs with Nested Locks .
publications
SEP Award 2017
Congratulations to the UnicornPL project teams on winning the SEP award 2017!
ESA 2017
On the Complexity of Bounded Context Switching .
publications
MFCS 2017
Domains for Higher-Order Games .
publications
MFCS 2017
On the Upward/Downward Closures of Petri Nets .
publications
SAS 2017
Effect Summaries for Thread-Modular Analysis .
publications
SAS 2017
Portability Analysis for Weak Memory Models. Porthos: One Tool for all Models .
publications
GI-Fachgruppe
Roland Meyer has been elected as the spokesperson of the GI-Fachgruppe Concurrency Theory .
NETYS 2017
Locality and Singularity for Store-Atomic Memory Models .
publications
Dr.-Ing. Georgel Calin
Congratulations on your successful defense!
BCS/CHPC Distinguished Dissertation Award
The thesis “Verification of Message Passing Concurrent Systems” (by Emanuele D'Osualdo) received the BCS/CHPC Distinguished Dissertation Award
in 2016.
PDF
NWPT 2016
Thread Summaries for Lock-Free Data Structures .
publications
FSTTCS 2016
Summaries for Context-Free Games .
publications
D-CON 2017
Roland Meyer will speak at the D-CON workshop.
EATCS Distinguished Dissertation Award
The thesis “Monoids as Storage Mechanisms” (by Georg Zetzsche) received the EATCS Distinguished Dissertation Award
in 2016.
PDF
Marktoberdorf 2016
Sebastian Wolff was accepted to the Marktoberdorf Summer School.
MEMICS 2016
Roland Meyer will speak at the MEMICS workshop.
Carl Zeiss
Our project ArchiV: Architecture-aware Verification has been granted.
research
LICS 2016
Complexity of Regular Abstractions of One-Counter Languages .
publications
LICS 2016
First-Order Logic with Reachability for Infinite-State Systems .
publications
UPMARC 2016
Roland Meyer will speak at the UPMARC summer school.
CONCUR 2017
Roland Meyer is a co-chair of the conference.
ESOP 2016
On Hierarchical Communication Topologies in the π-calculus .
publications
Best teaching award SoSe 2015
Our Bachelor's course Logik received the best teaching award.
VMCAI 2016
Pointer Race Freedom .
publications
FSTTCS 2015
What's Decidable about Availability Languages? .
publications
RP 2015
The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets .
publications
Best student paper at ICALP 2015
An approach to computing downward closures .
publications
ACM TECS
Memory-Model-Aware Testing - a Unified Complexity Analysis .
publications
NETYS 2015
Antichains for Recursive Program Verification .
publications
CCDP 2015
Roland Meyer will give an invited talk. More about the workshop
can be found
here .
MM 2015
Roland Meyer will give an invited talk. More about the workshop
can be found
here .
TACAS 2016
Roland Meyer is a member of the programme committee.
STACS 2015
Computing downward closures for stacked counter automata .
publications
CONCUR 2015
Roland Meyer is a member of the programme committee.
More about the conference
can be found
here .
ACSD 2015
Roland Meyer is a co-chair of the programme committee.
More about the conference
can be found
here .
FASE 2015
Lazy TSO Reachability .
publications
INFINITY 2014
Roland Meyer will give an invited talk. More about the workshop
can be found
here .
Best paper at ACSD 2014
Memory-Model-Aware Testing - a Unified Complexity Analysis .
publications
CONCUR 2014
Bounds on Mobility .
publications
MFCS 2014
The monoid of queue actions .
publications
weacon
Research training group Weak Consistency .
weacon
ICALP 2014
Robustness against Power is PSPACE-complete .
publications
STACS 2014
On Boolean closed full trios and rational Kripke frames .
publications
DFG
Our project R2M2: Robustness against Relaxed Memory Models has been granted.
research
ACSD 2014
Roland Meyer is a member of the programme committee. More about the conference
can be found
here .
Best teaching award SoSe 2013
Our Bachelor's course Logik received the best teaching award.
FSTTCS 2013
A Theory of Partitioned Global Address Spaces .
publications
LMCS
A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets .
publications
MFCS 2013
Semilinearity and Context-Freeness of Languages Accepted by Valence Automata .
publications
CONCUR 2013
A Theory of Name Boundedness .
publications
ICALP 2013
Rational Subsets and Submonoids of Wreath Products .
publications
ICALP 2013
Silent Transitions in Automata with Storage .
publications
SAS 2013
Static Provenance Verification for Message Passing Programs .
publications
ESOP 2013
Checking and Enforcing Robustness against TSO .
publications
TACAS 2014
Roland Meyer is a member of the programme committee. More about the conference
can be found
here .
DAAD-PROCOPE
Our project ROIS: Robustness under Realistic Instruction Sets has been granted.
research
LMCS
Petri Net Reachability Graphs: Decidability Status of FO Properties .
publications
ACSD 2013
Roland Meyer is a member of the programme committee. More about the conference
can be found
here .
Trencher
Our tool for checking robustness against TSO is available for download.
Trencher
Best paper at ACSD 2012
An Algorithmic Framework for Coverability in Well-Structured Systems .
publications
CONCUR 2012
A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets .
publications
Best paper at ETAPS 2012
Language-Theoretic Abstraction Refinement was awarded best paper from EAPLS.
publications
YR-CONCUR 2012
Roland Meyer is a member of the programme committee. More about the workshop
can be found
here .
INFINITY 2012
Roland Meyer is a member of the programme committee. More about the workshop
can be found
here .
FSTTCS 2011
Petri Net Reachability Graphs: Decidability Status of FO Properties .
publications
ACSD 2012
Roland Meyer is a member of the programme committee. More about the conference
can be found
here .
D-CON 2012
will be organised by the Concurrency Theory Group. The workshop takes place on the 08th and 09th of March 2012. More about the workshop
can be found
here .
YR-CONCUR 2011
Roland Meyer is a member of the programme committee. More about the workshop
can be found
here .
Theorietag 2011
Georg is giving an invited talk on erasing productions in grammars with regulated rewriting.
Homepage
ICALP 2011
Deciding robustness against total store ordering .
publications
ICALP 2011
On the capabilities of grammars, automata and transducers controlled by monoids .
publications
DLT 2011
A sufficient condition for erasing productions to be avoidable .
publications
ACSD 2011
Roland Meyer is a member of the programme committee. More about the conference
can be found
here .
CONCUR 2010
Kleene, Rabin, and Scott are available .
publications
ICALP 2010
The downward-closure of Petri net languages .
publications
CAV 2010
Petruchio: from dynamic networks to nets .
publications