Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
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.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:20 | |||
10:40 20mTalk | A Pure Demand Operational Semantics with Applications to Program Analysis OOPSLA 2024 Scott F. Smith The Johns Hopkins University, Robert Zhang The University of Texas at Austin, The Johns Hopkins University Link to publication DOI Pre-print | ||
11:00 20mTalk | 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 DOI Pre-print | ||
11:20 20mTalk | 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 DOI | ||
11:40 20mTalk | 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 DOI | ||
12:00 20mTalk | 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 DOI Pre-print |