Gillian-C: Introduction

important

Everything this section is true at the time of artifact submission for PLDI 2020 on 28th February 2020.

Gillian-C is the instantiation of Gillian to the C language. More precisely, CompCert-C). It can be found in the Gillian-C folder of the repository.

In this section, we start by describing its structure and then explain how to write symbolic tests.