Gillian, Part I: a multi-language platform for symbolic execution
File(s)3385412.3386014.pdf (471.53 KB)
Published version
Author(s)
Fragoso Santos, José
Maksimović, Petar
Ayoun, Sacha-Elie
Gardner, Philippa
Type
Conference Paper
Abstract
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 descrip- tion. We prove a parametric soundness result, introducing restriction on abstract states, which generalises path condi- tions used in classical symbolic execution. We instantiate Gillian 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.
Date Issued
2020-06-15
Date Acceptance
2020-02-27
Citation
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020, pp.927-942
ISBN
9781450376136
Publisher
Association for Computing Machinery
Start Page
927
End Page
942
Journal / Book Title
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
Copyright Statement
©2020 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution International 4.0 License.
https://creativecommons.org/licenses/by/4.0/
https://creativecommons.org/licenses/by/4.0/
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
GCHQ
Facebook
GCHQ
Grant Number
EP/K008528/1 - RG65358
EP/K008528/1
EP/R034567/1
Verified High Assurance Software RFA20784
Continuous Reasoning Call
RFA20789 / 4214910
Source
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)
Publication Status
Published
Start Date
2020-06-15
Finish Date
2020-06-20
Coverage Spatial
London, UK