diff --git a/publications.bib b/publications.bib index dd4ba3385c33bc727580b98faec42197468873b4..4537e1546e1600080eddb621b4337522107576d0 100644 --- a/publications.bib +++ b/publications.bib @@ -1726,6 +1726,29 @@ month = {05}, file = { Dinsdale-Young2010Locality.techreport.pdf:PDF}, } +@InProceedings{FragosoSantos2020Gillian, +author = {Jos{\'{e}} {Fragoso Santos} and Petar Maksimovi\'{c} and Sacha{-}{\'{E}}lie Ayoun and Philippa Gardner}, +title = { Gillian, Part I: A Multi-language Platform for Symbolic Execution }, +booktitle = { Proceedings of the 41st ACM SIGPLAN +International Conference on Programming Language Design and Implementation +(PLDI ’20), June 15–20, 2020, London, UK }, +year = {2020}, +doi = {10.1145/3385412.3386014}, +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 +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.}, +} + + @Comment{jabref-meta: databaseType:bibtex;}