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 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
10:36 - 12:04: Separation Logic and Memory SemanticsResearch Papers at Sala II Chair(s): Ilya SergeyYale-NUS College and National University of Singapore | |||
10:36 - 10:58 Talk | Iron: Managing Obligations in Higher-Order Concurrent Separation Logic Research Papers Aleš BizjakAarhus University, Daniel Gratzer, Robbert KrebbersDelft University of Technology, Lars BirkedalAarhus University Link to publication DOI Media Attached File Attached | ||
10:58 - 11:20 Talk | JaVerT 2.0: Compositional Symbolic Execution for JavaScript Research Papers José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela SampaioImperial College London, UK, Philippa GardnerImperial College London Link to publication DOI Media Attached File Attached | ||
11:20 - 11:42 Talk | ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS Research Papers Alasdair ArmstrongUniversity of Cambridge, Thomas BauereissUniversity of Cambridge, Brian CampbellUniversity of Edinburgh, Alastair ReidArm Ltd, Kathryn E. GrayUniversity of Cambridge, Robert M. NortonUniversity of Cambridge, Prashanth MundkurSRI International, Mark WassellUniversity of Cambridge, Jon FrenchUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Shaked FlurUniversity of Cambridge, Ian StarkThe University of Edinburgh, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Peter SewellUniversity of Cambridge Link to publication DOI Media Attached File Attached | ||
11:42 - 12:04 Talk | Exploring C Semantics and Pointer Provenance Research Papers Kayvan MemarianUniversity of Cambridge, Victor B. F. GomesUniversity of Cambridge, UK, Brooks DavisSRI International, Stephen KellUniversity of Kent, Alexander RichardsonUniversity of Cambridge, Robert N. M. WatsonUniversity of Cambridge, Peter SewellUniversity of Cambridge Link to publication DOI Media Attached File Attached |