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:Logic-based frameworks for automated verification of programs with dynamically allocated data structures
Speaker:Cezara Dragoi
coming from:IST Austria
Speakers Bio:Cezara is a Romanian-born computer scientist living in Austria. She is currently a post-doctoral researcher at IST Austria, in the group of Tom Henzinger. In 2011 she was awarded a Ph.D. from the Department of Computer Science at the University of Paris-Diderot (Paris 7), LIAFA, under the advising of Ahmed Bouajjani. Cezara's research focuses on software verification, and in particular on static analyses techniques for programs with dynamically allocated data structures. She has been a teaching and research assistant at the University of Bucharest and at the Romanian Institute of Mathematics.
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, 27 March 2014
Time:10:30
Duration:90 Minutes
Location:Kaiserslautern
Building:G26
Room:113
Abstract
Dynamically allocated data structures are heavily used in software nowadays, to organize and facilitate the access to data. This poses new challenges to software verification, due to various aspects, either related to the control structure or to the data.
In this talk, we present logic-based frameworks for automatic verification of programs manipulating data structures that store unbounded data. First, we are concerned with designing decidable logics, that can be used to automate deductive verification in the Hoare-style of reasoning. This method relies on user provided annotations, such as loop invariants. Second, we introduce static analyses, that can automatically synthesize such annotations. Classically, static analysis has been used to prove correctness of non-functional properties, such as null pointer deference. In this talk, we present static analyses, that can prove complex functional properties describing the values stored in the data structure.
Contact
Name(s):
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):
  • Susanne Girard, 03/19/2014 12:30 PM -- Created document.