[TYPES/announce] SyGuS-COMP 2019 Call for Solvers and Benchmarks Submission

[Dana Fisman]

Important Dates:

1 May 2019: Benchmark submission deadline [bechmarks submission link
<https://docs.google.com/forms/d/e/1FAIpQLScyPUPiCJR3W2cIS4b18ckd1gOsSSQg_3RM1mVSknFxRiX9Vw/viewform>
].

1 June 2019: Deadline for first version of solvers [solvers submission link
<https://docs.google.com/forms/d/e/1FAIpQLSdCLEMqDCFRswq1IktXjlHD-jSZDTWR5RmoAksWaxxMCKkSJQ/viewform>
].

14 June 2019: Deadline for final version of solvers and for solver
description

7 July 2019: Author notification

13/14 July 2019: Solvers presentation (at SYNT workshop)

Call for Participation:

This is a call for participation for the 6th Syntax-Guided Synthesis
Competition to be organized as a satellite event of SYNT & CAV 2019 in New
York City.

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 implementation. The motivation is twofold. First, narrowing the
space of implementations makes the synthesis problem more tractable.
Second, providing a specific syntax can potentially lead to better
optimizations.

The input to the syntax-guided synthesis problem (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.

There has been a lot of recent interest in both using SyGuS solvers for
various synthesis applications and developing different solving algorithms.
Despite significant progress in solution strategies in the last few years,
synthesis remains a challenging problem. Last year, in the general track,
more than 25% of the problems were unsolved, and we welcome solvers that can
advance the state of the art.

Tracks:

This year's competition will have 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. This year's SyGuS competition will use a
lightly modified version of the SyGuS input format that was used in
previous competitions. The new format is more compliant with SMT-LIB
version 2.6, includes minor changes to the concrete syntax for commands,
and eliminates several deprecated features of the previous format. A
comprehensive description of the new input format and its differences with
respect to the previous format is available in the reference document “The
SyGuS Language Standard Version 2.0”, available here
<http://sygus.org/assets/pdf/SyGuS-IF_2.0.pdf>.

Benchmarks for the competition:

We will evaluate the solvers on a subset of public benchmarks and some
secret benchmarks. The domains of benchmarks include bit-vector
manipulation, concurrency, robotics, string transformations, invariant
generation, program repair and cryptographic circuits. We are still
finalizing the set of benchmarks, and would appreciate your contribution to
the benchmarks as well.

Evaluation:

Evaluation of the solvers will be done on the StarExec system (200 dual
quad-core machines with 256GB memory each). The solvers would be run with a
TIMEOUT value. The SyGuS-correctness checker, as well as the solvers from
last year's competition are available on the SyGuS community at StarExec.
Candidate participants are invited to register on StarExec where they can
easily compare their solvers to the previous ones against the public
benchmarks.

Scoring:

The scoring system is per track and as follows. A solver that solved N
benchmarks in the track, out of which F benchmarks among the fastest
(according to the pseudo-logarithmic scale used in previous competitions)
and S benchmarks with an expression size among the smallest (according to
the pseudo-logarithmic scale used in previous competitions) will receive
the score 5*N+3*F+1*S. The solver with highest score will be announced the
winner.

Tool Submission and Description:

We expect the tool developers to test their solvers on the public
benchmarks, and submit the solver binaries by the Solver submission
deadline. Each solver submission should be accompanied by a 1-2 page (IEEE
format) description of the key ideas of the solvers.

Licensing of Tools and Benchmarks:

All benchmarks will be made public after the competition. We encourage the
tool developers to make their solvers open-source, but participants are
welcomed to submit binaries of proprietary tools as well.

Organization:

The competition was initiated as part of NSF Expeditions in Computing
project ExCAPE, and is organized by Rajeev Alur (University of
Pennsylvania), Dana Fisman (Ben-Gurion University), Saswat Padhi
<http://saswatpadhi.github.io/> (University of California, Los Angeles), Andrew
Reynolds <http://homepage.cs.uiowa.edu/~ajreynol/> (University of
Iowa), Rishabh
Singh (Google Brain), and Abhishek Udupa (Microsoft). For more information
see the sygus <http://www.sygus.org> webpage. For questions regarding the
competition 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/20190312/41d3bf09/attachment-0001.html>