Theoretical Computer Science

Theoretical Aspects of Verification

We work on computability and complexity results underlying verification tasks and verification algorithms that apply to classes of models.

Team:

Roland Meyer, Emanuele D'Osualdo, and Georg Zetzsche

Publications:

• First-order logic with reachability for infinite-state systems, by Emanuele D'Osualdo, Roland Meyer, and Georg Zetzsche.
  In Proceedings of LICS 2016.
  PDF | DOI

• An Algorithmic Framework for Coverability in Well-Structured Systems, by Tim Strazny and Roland Meyer.
  In Proceedings of ACSD 2012.
  ACSD 2012 best paper award.
  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

• Petri Net Reachability Graphs: Decidability Status of FO Properties, by Ph. Darondeau, S. Demri, Roland Meyer, and C. Morvan.
  In Proceedings of FSTTCS 2011.
  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

• Petri Net Reachability Graphs: Decidability Status of FO Properties, by Ph. Darondeau, S. Demri, Roland Meyer, and C. Morvan.
  Logical Methods in Computer Science, 2012.
  BibTeX