Toward Tool-Independent Summaries for Symbolic Execution (ECOOP 2023 - Research Papers) - ECOOP 2023

Mon 17 - Fri 21 July 2023 Seattle (University of Washington campus), Washington, United States

co-located with ECOOP and ISSTA 2023

Who

Frederico Ramos, Nuno Sabino, Pedro Adão, David Naumann, José Fragoso Santos

Track

ECOOP 2023 Research Papers

Time Zone

The program is currently displayed in (GMT-07:00) Pacific Time (US & Canada).

Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Thu 20 Jul 2023 14:45 - 15:00 at Habib Classroom (Gates G01) - ECOOP 5: Synthesis Chair(s): Karine Even-Mendoza

Abstract

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.

DOI

https://doi.org/10.4230/LIPIcs.ECOOP.2023.24

Frederico Ramos

Instituto Superior Técnico

Nuno Sabino

Instituto Superior Técnico, Carnegie Mellon University

Portugal

Pedro Adão

IST-ULisboa and Instituto de Telecomunicações

Portugal

David Naumann

Stevens Institute of Technology

United States

José Fragoso Santos

INESC-ID/Instituto Superior Técnico, Portugal

Time Zone

The program is currently displayed in (GMT-07:00) Pacific Time (US & Canada).

Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Thu 20 Jul
Displayed time zone: Pacific Time (US & Canada) change

	13:30 - 15:00	ECOOP 5: SynthesisResearch Papers at Habib Classroom (Gates G01) Chair(s): Karine Even-Mendoza King’s College London

	13:30 15m Talk		Synthesis-Aided Crash Consistency for Storage Systems Research Papers 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 Washington DOI
	13:45 15m Talk		Synthesizing Conjunctive Queries for Code Search Research Papers 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 Technology DOI
	14:00 15m Talk		Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution Research Papers 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 Lisbon DOI
	14:15 15m Talk		Building Code Transpilers for Domain-Specific Languages Using Program Synthesis Research Papers Sahil Bhatia University of California, Berkeley, Sumer Kohli UC Berkeley, Sanjit Seshia UC Berkeley, Alvin Cheung University of California at Berkeley DOI
	14:30 15m Talk		Do Machine Learning Models Produce TypeScript Types that Type Check? Research Papers Ming-Ho Yee Northeastern University, Arjun Guha Northeastern University and Roblox Research DOI Media Attached File Attached
	14:45 15m Talk		Toward Tool-Independent Summaries for Symbolic Execution Research Papers 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, Portugal DOI