Cezara Dragoi

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

(Vortrag im Rahmen der "MPI Distinguished Lecture Series" in Kooperation mit dem Fachbereich Informatik)

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.

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.