MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Logic-based frameworks for automated verification of programs with dynamically allocated data structures

Cezara Dragoi
IST Austria
SWS Colloquium

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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Thursday, 27 March 2014
10:30
90 Minutes
G26
113
Kaiserslautern

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

--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only

Susanne Girard, 03/19/2014 12:30 -- Created document.