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

Citations Over Time

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 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.

Related Papers

• → PACWON: A parallelizing compiler for workstations on a network(1998)
• Study and Two Types of Typical Usage of DataGrid Web Server Control(2005)
• Achieving Parameter of DBSCAN Based on Datagrid(2010)
• Using DataGrid Control to Realize DataBase of Querying in VB6.0(2000)
• Susquehanna Chorale Spring Concert "Roots and Wings"(2017)