Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Storage mechanisms and finite-state abstractions for software verification
Speaker:Georg Zetzsche
coming from:Université Paris-Diderot
Speakers 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).
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Thursday, 1 March 2018
Time:10:30
Duration:60 Minutes
Location:Kaiserslautern
Building:G26
Room:111
Abstract
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.
Contact
Name(s):Susanne Girard
Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:029
Meeting ID:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created:
Susanne Girard/MPI-SWS, 02/21/2018 02:19 PM
Last modified:
Uwe Brahm/MPII/DE, 03/01/2018 07:01 AM
  • Susanne Girard, 02/27/2018 11:09 AM
  • Susanne Girard, 02/21/2018 02:23 PM -- Created document.