We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build a new analysis tool for JavaScript that follows the semantics of the language without any simplifications, with support for whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning the tool is developed in a modular way, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of our tool on a number of JavaScript data-structure libraries, demonstrating the scalability of whole-program symbolic testing, an improvement over our previous work on JavaScript verification, and automatic creation of useful specifications using bi-abduction.
| JaVerT 2.0: Compositional Symbolic Execution for JavaScript (JaVerTPOPL19.pdf) | 2.17MiB |
Thu 17 JanDisplayed time zone: Belfast change
10:36 - 12:04 | Separation Logic and Memory SemanticsResearch Papers at Sala II Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore | ||
10:36 22mTalk | Iron: Managing Obligations in Higher-Order Concurrent Separation Logic Research Papers Aleš Bizjak Aarhus University, Daniel Gratzer , Robbert Krebbers Delft University of Technology, Lars Birkedal Aarhus University Link to publication DOI Media Attached File Attached | ||
10:58 22mTalk | JaVerT 2.0: Compositional Symbolic Execution for JavaScript Research Papers José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela Sampaio Imperial College London, UK, Philippa Gardner Imperial College London Link to publication DOI Media Attached File Attached | ||
11:20 22mTalk | ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS Research Papers Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Arm Ltd, Kathryn E. Gray University of Cambridge, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge Link to publication DOI Media Attached File Attached | ||
11:42 22mTalk | Exploring C Semantics and Pointer Provenance Research Papers Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Brooks Davis SRI International, Stephen Kell University of Kent, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge Link to publication DOI Media Attached File Attached | ||