PLDI 2020 (series) / PLDI Research Papers /
Gillian, Part I: A Multi-language Platform for Symbolic Execution
Fri 19 Jun 2020 13:20 - 13:40 at PLDI Research Papers live stream - Symbolic Execution Chair(s): Qirun Zhang
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 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.
Fri 19 JunDisplayed time zone: Pacific Time (US & Canada) change
Fri 19 Jun
Displayed time zone: Pacific Time (US & Canada) change
13:00 - 14:00 | Symbolic ExecutionPLDI Research Papers at PLDI Research Papers live stream Chair(s): Qirun Zhang Georgia Institute of Technology, USA | ||
13:00 20mTalk | Constant-Time Foundations for the New Spectre Era PLDI Research Papers Sunjay Cauligi University of California at San Diego, USA, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall University of California at San Diego, USA, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, USA, Tamara Rezk Inria, France, Gilles Barthe MPI for Security and Privacy, Germany / IMDEA Software Institute, Spain | ||
13:20 20mTalk | Gillian, Part I: A Multi-language Platform for Symbolic Execution PLDI Research Papers José Fragoso Santos INESC-ID/Instituto Superior Técnico, Portugal , Petar Maksimović Imperial College London, UK, Sacha-Élie Ayoun Imperial College London, UK, Philippa Gardner Imperial College London, UK DOI | ||
13:40 20mTalk | Efficient Handling of String-Number Conversion PLDI Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Julian Dolby IBM Research, USA, Petr Janků Brno University of Technology, Czechia, Hsin-Hung Lin Academia Sinica, Taiwan, Lukáš Holík Brno University of Technology, Czechia, Wei-Cheng Wu University of Southern California, USA | ||