Zafer Esen: Transformations for Verifying Programs with Heap-Allocated Data Structures

Abstract

Verifying programs that manipulate heap-allocated data structures is a long-standing challenge in software verification. This thesis summarises a series of five papers that advance the state of the art in automated verification of such programs through transformation-based approaches. The contributions include the development of a formal SMT-LIB theory of heaps to represent heap operations, the implementation of this theory in an automated verification tool for C programs, and novel invariant-based encodings that simplify reasoning about heap structures. The thesis further presents methods for automatically instrumenting programs to simplify verification tasks involving quantified properties and aggregations. All proposed techniques are fully automated and do not rely on user-provided annotations, enabling verification of heap-manipulating programs with quantified invariants that previously posed significant challenges to automated verification tools.