Venue

Ph.D. Thesis, Imperial College London, 2025

Publication date

May 2025

Identifiers

Authors

Abstract

This manuscript presents the mathematical foundations, implementation, instantiation, and evaluation of Gillian, a parametric compositional symbolic execution framework for reasoning about program correctness and incorrectness. Gillian supports three kinds of analyses: whole-program symbolic testing in the style of CBMC; semi-automatic compositional verification in the style of VeriFast or Viper; and automatic specification inference based on bi-abduction in the style of Infer:Pulse. To instantiate Gillian to a specific target language (TL), a tool developer must implement a symbolic state model, providing: for whole-program symbolic testing, a set of actions that capture the fundamental behaviours of the TL’s memory; for compositional verification, a set of core predicates (building blocks of a separation logic assertion language); and for specification inference, a set of fixes describing how errors resulting from missing resource can be fixed. We provide an interface for symbolic state models and an exhaustive list of properties they must satisfy to guarantee the soundness of the analyses. Gillian currently has four instantiations: real-world languages, namely JavaScript, C, and Rust; and a simple demonstrator language called Wisl. In this manuscript, we focus on the C and Rust instantiations, showing how they each leverage opportunities offered by Gillian’s unique and flexible parametricity. Specifically, Gillian-C encodes objects of the C heap into a novel tree representation that enables efficient compositional byte-level reasoning, and Gillian-Rust automates exotic separation logic reasoning specified by RustBelt and RustHornBelt and usually performed in Iris. The Gillian-C instantiation was used for several real-world case studies, successfully finding bugs in industrial-grade code, including the AWS codebase. Gillian-Rust was designed to enable hybrid Rust verification, where safe Rust is verified using the Creusot and the unsafe code is verified using Gillian. Preliminary evaluation shows that this prototype can verify small, non-trivial fragments of the Rust standard library with minor source code modification.

Source Materials