Skip to content
Snippets Groups Projects
Normal view Permalink
gillian.md 2.21 KiB
Newer Older
  • Learn to ignore specific revisions
    • pmaksimo's avatar
    gillian
    pmaksimo committed
    1 2 3 4 5 6 7 8 9 10 11 
    ---
title: Gillian
project_id: gillian
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 2
---

Gillian is a multi-language platform for the development
of compositional symbolic analysis tools. Gillian currently
    pmaksimo's avatar
    lots  
    pmaksimo committed
    12 
    supports three flavours of analysis: symbolic
    pmaksimo's avatar
    gillian
    pmaksimo committed
    13 14 15 16 17 18 19 
    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
    pmaksimo's avatar
    lots  
    pmaksimo committed
    20 21 22 23 
    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.
    pmaksimo's avatar
    gillian
    pmaksimo committed
    24 25 26 27 28 29 30 31 
    
#### 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,
    pmaksimo's avatar
    lots  
    pmaksimo committed
    32 
    which generalises path conditions of classic symbolic execution.
    pmaksimo's avatar
    gillian
    pmaksimo committed
    33 34 35 
    
#### Instantiations
    pmaksimo's avatar
    lots  
    pmaksimo committed
    36 
    In order to instantiate Gillian to a new TL,
    pmaksimo's avatar
    gillian
    pmaksimo committed
    37 
    the tool developer has to provide:
    pmaksimo's avatar
    lots  
    pmaksimo committed
    38 
    - a trusted compiler from the TL to GIL instantiated with the TL basic actions, preserving the TL memory model and semantics;
    pmaksimo's avatar
    gillian
    pmaksimo committed
    39 
    - an OCaml implementation of the concrete and symbolic memory models of the TL; and
    pmaksimo's avatar
    lots  
    pmaksimo committed
    40 
    - for the meta-theory, proofs of simple lemmas for the TL basic actions.
    pmaksimo's avatar
    gillian
    pmaksimo committed
    41 42 43 44 45 46 
    
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
    pmaksimo's avatar
    lots  
    pmaksimo committed
    47 48 49 50 51 52 53 54 55 56 57 58 
    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
[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/