Helmut Seidl graduated in Mathematics (1983) and received his Ph.D. degree in Computer Science (1986) from the Johann Wolfgang Goethe Universität, Frankfurt. He received his Dr. Habil. (1994) from the Universität des Saarlandes, Saarbrücken. 1994 he was appointed Full Professor at the University of Trier. Since 2003, he holds the chair for "Languages and Specification Formalisms" at TU München. From 2009 to 2018, he has been speaker of the research training group PUMA ("Programm- Und Modell-Analyse") and now is speaker of the research training group ConVeY ("Continuous Verification of CYber-Physical Systems"). His research interests include static analysis by abstract interpretation and model checking, efficient fixpoint algorithms, and expressive domains for numerical invariants. He has worked on dedicated analyses of concurrent and parametric systems, safety critical C programs, and cryptographic protocols. He is also interested in tree automata and corresponding classes of Horn clauses, in tree transducers and XML processing.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows. Desirable properties of these systems such as functional correctness or non-interference have conveniently been formulated as safety properties. Here, we go one step further. Our goal is to verify safety, and also to develop techniques for automatically synthesizing strategies to enforce safety. For that reason, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is equivalent to second-order quantifier elimination. For monadic games, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal invariants only. We identify a non-trivial sub-class where safety is decidable. For the general case, we provide meaningful abstraction and refinement techniques for realizing a CEGAR based synthesis loop.
Joint work with:
Christian Müller, TUM
Bernd Finkbeiner, Universität des Saarlandes

Mouna Litz

--email hidden

passcode not visible

logged in users only