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.
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.
Minimal proof effort
Gillian comes with parametric correctness results, meaning that you only need to prove correct what you implement, nothing more.