research interests

My works' underlying basic research question is the formal verification and synthesis of infinite systems. The latter naturally arise in the context of distributed systems, asynchronous programs, and concurrent software; but are also of theoretical interest.

I focus mainly on two different angles of attack:

1. first, theory based exhaustive methods (theory-to-practice)
   • investigation of the decidability/undecidability frontier for basic decision problems,
   • applying under-approximative techniques(e.g., bounded phases or semantic guarantees)
   • a view based on graph transformation systems to derive decidability results from graph properties, e.g., anti-patterns, regular graph grammars, or graph measures (like tree-width), as well as to base a system's semantic description on graph grammars
   • applying a game-theoretical perspective, especially in the context of synthesis questions
   • prototypical implementation for manageable (wrt. complexity and practical importance) subcases
2. second, applying semi-algorithmic solutions to practical problems
   • applying over-approximative techniques (e.g., CEGAR) depending on new abstraction and refinement techniques, for example path-invariants
   • implementation in a simple tool that is usable (and accessible) to the engineer (for model checking existing implementations and to support the specification of new protocols); see our McScM framework

3. keywords

   formal verification, model checking, synthesis, CEGAR, verification of protocols and asynchronous concurrent software, automata models (communicating automata, Petri nets, counter automata, queue automata, dynamic systems of pushdown automata, WSTS), formal languages for specifying models and specifications of complex, concurrent systems (e.g., temporal logics, message sequence charts), game theory, graph grammars, abstraction and refinement techniques, interpolation;