Gillian, Part I: A Multi-Language Platform for Symbolic Execution


José Fragoso Santos
Petar Maksimović
Sacha-Élie Ayoun
Philippa Gardner


We introduce Gillian, a platform for developing symbolic analysis tools for programming languages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is parametric on the memory model of the target language. We give a formal description of the symbolic analysis and a modular implementation that closely follows this description. We prove a parametric soundness result, introducing restriction on abstract states, which generalises path conditions used in classical symbolic execution. We instantiate to obtain trusted symbolic testing tools for JavaScript and C, and use these tools to find bugs in real-world code, thus demonstrating the viability of our parametric approach.


Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Publication Date