Gillian is a multi-language platform for the development of compositional symbolic analysis tools. Gillian currently supports three flavours of analysis: symbolic testing, full verification based on separation logic, and automatic compositional testing based on bi-abduction. These analysis are, for the first time, unified in a common symbolic execution engine.

Instantiation

At the core of Gillian is GIL, a simple goto intermediate language that is parametric on the memory model of the source language: that is, on the set of basic actions capturing the fundamental ways in which source programs interact with their memories.

In order to instantiate Gillian to a new source language, the tool developer has to provide:

  • a trusted compiler from source to GIL instantiated with the source language’s basic actions and preserving the language’s memory model and semantics;
  • an OCaml implementation of the concrete and symbolic memory models of the source language; and
  • for the meta-theory, proofs of simple lemmas for the language’s basic actions.

So far, we have instantiated Gillian to JavaScript and C.

Correctness (and Incorrectness)

The symbolic execution of Gillian is fully formalised, with the implementation closely following the formalisation. The correctness results are, for the first time, stated and proven parametrically, independently of the source language. This has been made possible by a novel concept of restriction, which generalises path conditions of classic symbolic execution.

In lockstep with foundational research on Compositional Symbolic Execution, Gillian is also the first tool to support both correctness and incorrectness reasoning in a single execution engine.

Debugging

Gillian has become the foundation for new work on visual, interactive debugging for compositional symbolic execution. All Gillian instantiations can launch a debugging session in VSCode for symbolic execution of GIL. Source-level debugging can be provided by enhancing an instantiation’s compiler with necessary annotations, and providing a lifter module to interpret annotated GIL steps as they are executed. Enhancing a Gillian instantiation with annotations during compilation, and a lifter module to progess GIL steps, a source-level debugger for Gillian in VSCode is provided.

Alongside its use in research, Gillian’s debugger has been used to support multiple labs on Gillian and Compositional Symbolic Execution.

Research Support

Gillian is supported by Gardner’s UKRI Established Career Fellowship “VeTSpec: Verified Trustworthy Software Specification”, Facebook, and GCHQ. It was previously supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems.

People

Photo of Sacha Ayoun
Sacha
Ayoun
Photo of José Fragoso Santos
José
Fragoso Santos
Photo of Philippa Gardner
Philippa
Gardner
Photo of Nat Karmios
Nat
Karmios
Photo of Petar Maksimović
Petar
Maksimović

Recent Publications

  1. Gillian Debugging: Swinging Through the (Compositional Symbolic Execution) Trees

    Proceedings of the 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, held as part of the International Joint Conferences on Theory and Practice of Software (TACAS 2026), pp. 195–214

  2. Symbolic Debugging with Gillian

    Proceedings of the 1st ACM International Workshop on Future Debugging Techniques, pp. 1–2

  3. Gillian, Part I: A Multi-language Platform for Symbolic Execution

    Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’20), June 15–20, 2020, London, UK