A Multi-Language Platform for Compositional Symbolic Analysis

[object Object]

GIL: General Intermediate Language

Gillian uses an intermediate language called GIL. GIL is a simple goto language parametric on the basic actionsof the memory model of the target language.

[object Object]

Focus on what matters

Give Gillian a compiler from your target language (TL) to GIL and an OCaml implementation of the TL symbolic memory model, and obtain several powerful symbolic analysis tools in return.

[object Object]

Minimal proof effort

Gillian comes with parametric correctness results, meaning that you only need to prove correct what you implement, nothing more.