Gillian: Compositional Symbolic Execution for All
Programming Languages
2020-01-16 v1 Logic in Computer Science
Abstract
We present Gillian, a language-independent framework for the development of compositional symbolic analysis tools. Gillian supports three flavours of analysis: whole-program symbolic testing, full verification, and bi-abduction. It comes with fully parametric meta-theoretical results and a modular implementation, designed to minimise the instantiation effort required of the user. We evaluate Gillian by instantiating it to JavaScript and C, and perform its analyses on a set of data-structure libraries, obtaining results that indicate that Gillian is robust enough to reason about real-world programming languages.
Keywords
Cite
@article{arxiv.2001.05059,
title = {Gillian: Compositional Symbolic Execution for All},
author = {José Fragoso Santos and Petar Maksimović and Sacha-Élie Ayoun and Philippa Gardner},
journal= {arXiv preprint arXiv:2001.05059},
year = {2020}
}