Detail

Shape Analysis of Low-Level List Manipulating Programs via Symbolic Memory Graphs

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.