by Georg Zetzsche

(Institut de Recherche en Informatique Fondamentale, Paris)
hosted by Rupak Majumdar

"Storage mechanisms and finite-state abstractions for software verification"

( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)

A popular approach to automatic program verification is to come up with an abstraction that reflects pertinent properties of the program. This abstraction is drawn from a class of formal models that is amenable to analysis. In the plethora of existing formal models, the aspects of programs that can be represented faithfully are typically determined by the infinite dimension of its state space, its storage mechanism. A central theme of my recent research is to obtain general insights into how the structure of the storage mechanism affects the analysis of a formal model. In the first part of my talk, I will survey results on an overarching framework of storage mechanisms developed in my doctoral work. It encompasses a range of infinite-state models and permits meaningful characterizations of when a particular method of analysis is applicable. Another current focus of my work concerns finite-state abstractions of infinite-state models. On one hand, these can be over- or under-approximations that are more efficient to analyze than infinite-state systems. On the other hand, they can serve as easy-to-check correctness certificates that are produced instead of yes-or-no answers to a verification task. Thus, the second part of my talk will be concerned with results on computing downward closures and related finite-state abstractions.

Bio: Georg Zetzsche is a post-doc at the Institut de Recherche en Informatique Fondamentale (IRIF) in Paris and holds a fellowship of the Fondation Sciences Mathématiques de Paris. Before that, he was a post-doc at Laboratoire Spécification et Vérification (LSV) in Cachan with a fellowship from the German Academic Exchange Service (DAAD). He received his PhD in 2015 from the University of Kaiserslautern. For his doctoral work, he received the Distinguished Dissertation Award of the European Association for Theoretical Computer Science (EATCS).

Time:	Thurday, 01.03.2018, 10:30 a.m.
Place:	MPI-SWS Kaiserslautern Paul Ehrlich Str. 26, room 111
Video:	Simultaneous video cast MPI-SWS Saarbrücken, room 029