What is Gillian?

Gillian is a framework for reasoning about program correctness and incorrectness, based on Compositional Symbolic Execution and inspired by ideas from Separation Logic.

A Gillian instantiation is created by providing the Gillian core library with a memory model implementation and a compiler from the source language to Gillian's intermediate language, GIL. A number of existing instantiations are available.

If you'd like to try out Gillian for yourself, take a look at the labs & tutorials.

To work on Gillian itself, compile Gillian from source and then check out the development instructions.

Gillian is the focus of numerous academic publications.