Newer
Older
---
title: Gillian
project_id: gillian
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 2
---
[Gillian](https://gillianplatform.github.io/) is a multi-language platform for the development
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,
- 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
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"][VeTSpec], Facebook,
and GCHQ. It was previously supported by the EPSRC programme grant
[EP/K008528/1]: [REMS: Rigorous Engineering of Mainstream Systems][REMS].
[VeTSpec]: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/R034567/1
[EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1