We propose a method that transforms a C program manipulating lists via low-level pointer statements into an equivalent program where the lists are manipulated via calls of standard high-level container operations like push_back, pop_front, etc. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers. The resulting program where low-level pointer statements are summarized into high-level container operations is more understandable and better suitable for program analyses since the burden of analysing low-level pointer manipulations gets removed. We have implemented our approach and successfully tested it through a number of experiments, including experiments showing that our method can indeed be used to ease program analysis by separating shape analysis from analysing data-related properties. The result is a joint work with Kamil Dudka, Lukas Holik, and Petr Peringer from Brno University of Technology and Marek Trtik from Verimag, Grenoble.
Tomas Vojnar received his PhD at the Brno University of Technology (BUT) in 2001. From 2001 to 2003, he worked as a postdoc researcher at LIAFA, Université Paris Diderot. Since 2003, he works at the Faculty of Information Technology of BUT. He defended his habilitation thesis in 2007 and became a full professor in 2012. His research focuses mainly on automated verification, especially over infinite-state and concurrent systems. In the former area, his work has included formal verification of parameterized systems, abstract regular model checking, and shape analysis of programs with pointers and dynamic linked data structures. He has also worked on efficient ways of dealing with various kinds of non-deterministic automata and logics, with applications in the above mentioned verification approaches. As for concurrent programs, he has mainly worked in the area of their noise-based testing and dynamic analysis, self-healing, as well as applications of search techniques in noise-based testing. He has (co-)authored over 100 scientific publications as well as multiple software tool prototypes (e.g., Forester, Predator, SearchBestie, AnaConDA, Spen, or Slide). These works won multiple best paper awards, such as the EATCS Best Theory Paper Award of ETAPS'10, the best tool paper of RV'12, as well as multiple medals in the international software verification competition SV-COMP'12-15, including a Goedel medal at the FLoC Olympic Games 2014.
This talk is organized by the Vienna PhD School of Informatics and part of the lecture series „Current Trends in Computer Science“.