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

[Dana Fisman]

*Important Dates:*
1 May 2018: Benchmark submission deadline
1 June 2018: Deadline for first version of solvers
14 June 2018: Deadline for final version of solvers and for solver
description
7 July 2018: Author notification
14 July 2018: Awards ceremony (at FLoC Olympic Games)
18 July 2018: Solvers presentation (at SYNT workshop)


*Call for Participation:*This is a call for participation for the 5th
Syntax-Guided Synthesis Competition to be organized as a satellite event of
SYNT & CAV 2018 and as part of FLoC olympic games.

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.
The SyGuS competition (SyGuS-Comp'18) will allow solvers to compete on a
collection of benchmarks and advance the state-of-the-art for
program-synthesis tools.


*Tracks:*This year's competition will have 4 tracks: 1) General SyGuS track,
2) Invariant Synthesis track, 3) Conditional Linear Integer Arithmetic
track, and 4) Programming By Examples (PBE). More details about the tracks
can be found in the extended SyGuS-IF
<http://sygus.seas.upenn.edu/files/SyGuS-Syntax-SyGuSCOMP'15.pdf>. The
results of the 4th SyGuS competition can be found here
<http://www.sygus.org/files/SyGuSComp2017.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, including bit-vector algorithms,
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 - an honor which will be accompanied by a FLoC olympic medal.


*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 (Penn), Dana Fisman (Ben-Gurion
University), Rishabh Singh (Google), and Abhishek Udupa (Microsoft). 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/20180404/77746c64/attachment-0001.html>