Theoretical Computer Science

Language-Theoretic Verification

We develop verification and synthesis algorithms that are based on concepts from formal language theory. Languages directly capture the (un)desired behaviour in a system, and thus offer a global understanding of the interplay among instructions.

Team:

Roland Meyer, Sebastian Muskalla, Prakash Saivasan, and Georg Zetzsche

Publications:

• What's Decidable about Availability Languages?, by Parosh Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi.
  In Proceedings of FSTTCS 2015.
  PDF | DOI | BibTeX

• Antichains for Recursive Program Verification, by Lukas Holik and Roland Meyer.
  In Proceedings of NETYS 2015.
  PDF | Correction | DOI | BibTeX

• Language-Theoretic Abstraction Refinement, by Zhenyue Long, Georgel Calin, Rupak Majumdar, and Roland Meyer.
  In Proceedings of FASE 2012.
  ETAPS 2012 best paper award by EAPLS.
  DOI | www | BibTeX

• Kleene, Rabin, and Scott are available, by Jochen Hoenicke, Roland Meyer, and Ernst-Rüdiger Olderog.
  In Proceedings of CONCUR 2010.
  PDF | DOI | BibTeX

• The downward-closure of Petri net languages, by Peter Habermehl, Roland Meyer, and Harro Wimmel.
  In Proceedings of ICALP 2010.
  Slides | PDF | DOI | BibTeX

Funding:

TU Kaiserslautern: PhD Program at the Department for Computer Science