[TYPES/announce] Call for SyGuS Benchmarks and Language Extensions

[Andrew Reynolds]

Call for SyGuS Benchmarks and Language Extensions

Background:

The classical formulation of the program-synthesis problem is to find a
program that meets a correctness specification given as a logical
formula. Recent work on program synthesis and program optimization
illustrates many potential benefits of allowing the user to supplement
the logical specification with a syntactic template that constrains the
space of allowed implementations. The Syntax-Guided Synthesis (SyGuS)
problem is a standardized format for specifying the computational
problem at the core of such efforts.

The input to SyGuS consists of a background theory, a semantic
correctness specification for the desired program given by a logical
formula, and a syntactic set of candidate implementations given by a
grammar. The computational problem then is to find an implementation
from the set of candidate expressions that satisfies the specification
in the given theory. The formulation of the problem builds on SMT-LIB.

SyGuS Competition Status:

Aimed at stimulating innovations in SyGuS solution techniques,
SyGuS-Comp, a competition of solvers for SyGuS benchmarks, has been held
every year from 2014 to 2019. There has been continued interest  in both
using SyGuS solvers for various synthesis applications and using SyGuS
benchmarks for evaluating new solution strategies. However, we
anticipate that this year there will be no significantly new solvers
that are ready to compete. Hence, we will not be organizing SyGuS-Comp
in 2020. To continue to provide useful infrastructure for advancing
research in program synthesis, instead, we are seeking new benchmarks
and proposals for extending the SyGuS language.

Extensions to SyGuS Language:

The most recent SyGuS competition, held in Summer 2019, had 5 tracks: 1)
General SyGuS track, 2) Invariant Synthesis track, 3) Conditional Linear
Integer Arithmetic track, and 4) Programming By Examples in Strings
theory and 5) Programming By Examples in BitVector theory. The input
format used in this competition, called "The SyGuS Language Version 2.0"
(https://sygus.org/assets/pdf/SyGuS-IF_2.0.pdf), is compliant with
SMT-LIB version 2.6. Based on requests from the synthesis researchers,
we are currently considering the following extensions and updates:

(1) Quantitative extensions of the SyGuS language: This includes the
addition of weight annotations to SyGuS grammars, support for
constraints over these weights, as well as a new command in the SyGuS
language (e.g. maximize-synth) to ask the solver to synthesize a
function that maximizes a given objective function.

(2) Table transformations:  We are working on syntax for a SMT-LIB
compliant theory of tables whose signature includes operations like
table join, filtering and aggregation. Upcoming SyGuS competitions will
incorporate a track for programming-by-examples (PBE) constraints over
this domain.

(3) Infeasibility for SyGuS conjectures: Future editions of the SyGuS
language standard will include further guidelines for solvers that can
prove that no solution exists for a SyGuS conjecture. Future editions of
SyGuS-Comp may include a track for such solvers.

(4) Broadening the scope of verification backends: Traditionally,
Satisfiability Modulo Theories (SMT) solvers are the verification
portion of SyGuS solvers. We are interested in incorporating and
standardizing other backend black-box tools for this purpose.

We welcome feedback and comments on the proposed extensions, as well as
suggestions for other features. Please submit all comments by email to
the organizers by September 1, 2020.

Benchmarks:

The SyGuS repository currently has over 2800 benchmarks. The domains of
benchmarks include bit-vector manipulation, concurrency, robotics,
string transformations, invariant generation, program repair and
cryptographic circuits. These benchmarks are publicly available, and
used by multiple research teams to evaluate new solver techniques. There
is always a need for growing the set of benchmarks, and we would
appreciate your contribution to this effort. New benchmarks can be
submitted by September 1, 2020 by email to the organizers.


Organization:

The SyGuS infrastructure and competition was initiated as part of NSF
Expeditions in Computing project ExCAPE, and is currently organized by
Rajeev Alur (University of Pennsylvania), Saswat Padhi (University of
California, Los Angeles), Andrew Reynolds (University of Iowa), Rishabh
Singh (Google Brain), and Abhishek Udupa (Microsoft). For more
information see the sygus webpage https://sygus.org/ . For questions
please contact the organizers at sygus-organizers at seas.upenn.edu.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20200630/e1f56248/attachment-0001.htm>