Title: Shape Analysis of Low-Level List Manipulating Programs via Symbolic Memory Graphs
By: Tomas Vojnar (Brno University of Technology)
Abstract:
In the talk we will introduce an approach to shape analysis of programs with linked lists using low-level memory operations. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. The approach that will presented is in particular based on a notion of the so called symbolic memory graphs, which is to some degree inspired by works on separation logic with higher-order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to support the various low-level memory operations. The approach was implemented in the Predator tool and successfully validated on multiple non-trivial case studies that are beyond the capabilities of other current fully automated shape analysis tools. The Predator tool has also won multiple medals in the international software verification competition SV-COMP. In the talk, we will further briefly mention a recently proposed approach for converting programs using low-level pointer operations to implement list containers to high-level container programs, which has been implemented on top of Predator and which allows one to simplify verification of such programs by separating the need to deal with pointers and other kinds of data.
Short bio:
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 analysis and 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, shape analysis of programs with pointers and dynamic linked data structures, as well as verification of hardware designs. 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, and 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, Slide, or dWiNA). 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.