Toward Tool-Independent Summaries for Symbolic Execution
We introduce a new symbolic reflection API for implementing tool-independent summaries for the symbolic execution of C programs. We formalise the proposed API as a symbolic semantics and extend two state-of-the-art symbolic execution tools with support for it. Using the proposed API, we implement 67 tool-independent symbolic summaries for a total of 26 libc functions. Furthermore, we present SumBoundVerify, a fully automatic summary validation tool for checking the bounded correctness of the symbolic summaries written using our symbolic reflection API. We use SumBoundVerify to validate 37 symbolic summaries taken from 3 state-of-the-art symbolic execution tools, angr, Binsec and Manticore, detecting a total of 24 buggy summaries.
Thu 20 JulDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00
|Synthesis-Aided Crash Consistency for Storage Systems
Jacob Van Geffen Veridise Inc., James Bornholt University of Texas at Austin, Emina Torlak Amazon Web Services and University of Washington, Xi Wang University of WashingtonDOI
|Synthesizing Conjunctive Queries for Code Search
Chengpeng Wang Hong Kong University of Science and Technology, Peisen Yao Zhejing University, Wensheng Tang Hong Kong University of Science and Technology, Gang Fan Ant Group, Charles Zhang Hong Kong University of Science and TechnologyDOI
|Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution
Henrique Botelho Guerra INESC-ID and IST, University of Lisbon, João F. Ferreira INESC-ID and IST, University of Lisbon, João Costa Seco NOVA-LINCS; Nova University of LisbonDOI
|Building Code Transpilers for Domain-Specific Languages Using Program Synthesis
Sahil Bhatia University of California, Berkeley, Sumer Kohli UC Berkeley, Sanjit Seshia UC Berkeley, Alvin Cheung University of California at BerkeleyDOI
|Do Machine Learning Models Produce TypeScript Types that Type Check?
Research PapersDOI Media Attached File Attached
|Toward Tool-Independent Summaries for Symbolic Execution
Frederico Ramos Instituto Superior Técnico, Nuno Sabino Instituto Superior Técnico, Carnegie Mellon University, Pedro Adão IST-ULisboa and Instituto de Telecomunicações, David Naumann Stevens Institute of Technology, José Fragoso Santos INESC-ID/Instituto Superior Técnico, PortugalDOI