[TYPES/announce] SyGuS-COMP 2015: Call for Benchmarks and Solvers

[Dana Fisman]

SyGuS-COMP 2015: 2nd Syntax Guided Synthesis Competition
                      Satellite event of CAV and SYNT 2015
                               http://www.sygus.org


Important Dates:


Benchmark Submission Deadline: 31 May 2015

Solver Submission Deadline: 15 June 2015

Competition Date: 28 June 2015

Results published: 10 July 2015

Solver Presentations: 18 July 2015 (with SYNT
<http://formal.epfl.ch/synt/2015/>)



Submission Links:


Benchmark submission <http://www.sygus.org/benchmark-reg-2015.html>

Solver submission <http://www.sygus.org/solver-reg-2015.html>


Call for Participation:

This is a call for participation for the Second Syntax-Guided Synthesis
Competition <http://www.sygus.org/> to be organized as a satellite event of
SYNT <http://formal.epfl.ch/synt/2015/>/CAV <http://i-cav.org/2015/> 2015.

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 SyGuS-Comp competition will allow solvers to compete on a collection of
benchmarks and advance the state-of-the-art for program-synthesis tools.
The competition is organized as part of NSF Expeditions in Computing project
ExCAPE <https://excape.cis.upenn.edu/> by Rajeev Alur (Penn), Dana Fisman
(Penn), Rishabh Singh (Microsoft Research) and Armando Solar-Lezama (MIT).
For questions regarding the competition please contact the organizers at
sygus-organizers at seas.upenn.edu.

Tracks


In addition to a general track (similar to last year's competition
<https://github.com/rishabhs/sygus-comp14/blob/master/docs/sygus-language.pdf?raw=true>),
we will also be having two special tracks: 1) Invariant Synthesis track,
and 2) Conditional Linear Integer Arithmetic track. The Invariant Synthesis
track would consist of invariant synthesis benchmarks over linear integer
arithmetic where the correctness specification would be structured in the
form of pre-condition, post-condition, and a transition relation. The
Conditional Linear Integer Arithmetic track would consist of synthesis
benchmarks where the grammar of candidate implementations will be fixed
generating expressions in the theory of linear integer arithmetic with
Boolean conditionals. [See here the enhanced SyGuS-IF
<http://www.sygus.org/files/SyGuS-Syntax-SyGuSCOMP'15.pdf> syntax.]


Benchmarks for the competition

We will evaluate the solvers on a subset of public benchmarks and some
secret benchmarks. The benchmarks domain areas include bit-vector
manipulation, including bit-vector algorithms, concurrency, robotics, and
invariant generation. We are still finalizing the set of benchmarks, and
would appreciate your contribution especially for the newer tracks of
invariant synthesis and conditional linear integer arithmetic. [benchmark
submission link <http://www.sygus.org/benchmark-reg-2015.html>]

Evaluation

Evaluation of the solvers will be done on the StarExec
<https://www.starexec.org/starexec/public/about.jsp> 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 two initial
solvers (enumerative and stochastic) are available on the SyGuS community
at StarExec. Candidate participants are invited to register to StarExec
where they can easily and discreetly compare their solvers to the initial
ones against the public benchmarks.

Scoring Scheme

The solvers scores will be based primarily on the number of benchmark
solved and the solving time, and secondarily on the succinctness of the
synthesized solution.

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. [solver submission link
<http://www.sygus.org/solver-reg-2015.html>]

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.


Best regards,
SyGuS-COMP15 Organizers
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20150510/93cdab1e/attachment-0001.html>