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.

GIL

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

Correctness

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 TL. This has been made possible by a novel concept of restriction, which generalises path conditions of classic symbolic execution.

Instantiations

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

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

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

Publications

We have recently published the first paper on Gillian at PLDI’20 (see below), which introduces the principles of Gillian, its core symbolic execution, and its symbolic testing.

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 Petar Maksimović
Petar
Maksimović

Recent Publications

  1. 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