This program is tentative and subject to change.

Wed 23 Oct 2024 11:00 - 11:20 at San Gabriel - Semantics Chair(s): Ilya Sergey

In top-down enumeration for program synthesis, abstraction-based pruning uses an abstract domain to approximate the set of possible values that a partial program, when completed, can output on a given input. If the set does not contain the desired output, the partial program and all its possible completions can be pruned. In its general form, abstraction-based pruning requires manually designed, domain-specific abstract domains and semantics, and thus has only been used in domain-specific synthesizers. This paper provides sufficient conditions under which a form of abstraction-based pruning can be automated for arbitrary synthesis problems in the general-purpose Semantics-Guided Synthesis (SemGuS) framework without requiring manually-defined abstract domains. We show that if the semantics of the language for which we are synthesizing programs exhibits some monotonicity properties, one can obtain an abstract interval-based semantics for free from the concrete semantics of the programming language, and use such semantics to effectively prune the search space. We also identify a condition that ensures such abstract semantics can be used to compute a precise abstraction of the set of values that a program derivable from a given hole in a partial program can produce. These precise abstractions make abstraction-based pruning more effective. We implement our approach in a tool, Moito, which can tackle synthesis problems defined in the SemGuS framework. Moito can automate interval-based pruning without any a-priori knowledge of the problem domain, and solve synthesis problems that previously required domain-specific, abstraction-based synthesizers— e.g., synthesis of regular expressions, CSV file schema, and imperative programs from examples.

This program is tentative and subject to change.

Wed 23 Oct

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

10:40 - 12:20
SemanticsOOPSLA 2024 at San Gabriel
Chair(s): Ilya Sergey National University of Singapore
10:40
20m
Talk
A Pure Demand Operational Semantics with Applications to Program Analysis
OOPSLA 2024
Scott F. Smith The Johns Hopkins University, Robert Zhang The Johns Hopkins University
Link to publication DOI Pre-print
11:00
20m
Talk
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
OOPSLA 2024
Keith J.C. Johnson University of Wisconsin–Madison, Rahul Krishnan University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison
11:20
20m
Talk
HOL4P4: mechanized small-step semantics for P4
OOPSLA 2024
Anoud Alshnakat KTH Royal Institute of Technology, Didrik Lundberg KTH Royal Institute of Technology and Saab AB, Roberto Guanciale KTH Royal Institute of Technology, Mads Dam KTH
11:40
20m
Talk
Semantics Lifting for Syntactic Sugar
OOPSLA 2024
Zhichao Guan Peking University, Yiyuan Cao Peking University, Tailai Yu Tsinghua University, Ziheng Wang , Di Wang Peking University, Zhenjiang Hu Peking University
12:00
20m
Talk
Synthesizing Formal Semantics from Executable Interpreters
OOPSLA 2024
Jiangyi Liu University of Wisconsin - Madison, Charlie Murphy University of Wisconsin–Madison, Anvay Grover University of Wisconsin-Madison, Keith J.C. Johnson University of Wisconsin–Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin-Madison