[TYPES/announce] SyGuS-COMP 2014: 2nd Call for Participation

[Rishabh Singh]

                      Second Call for Participation
SyGuS-COMP 2014: 1st Syntax Guided Synthesis Competition
                      Satellite event of CAV and SYNT 2014
                              FLoC Olympic Games
                      Vienna Summer of Logic 2014
                               http://www.sygus.org


Important Dates:

Solver Submission Deadline: 15 June 2014

Competition takes place: 28 June 2014

Results published: 10 July 2014

Awards: 21 July 2014 at the FLoC Awards Ceremony<http://vsl2014.at/olympics/>
Solver Presentations: 23-24 July 2014 (with
SYNT<http://vsl2014.at/meetings/SYNT-index.html>
)

Call for Participation:

This is 2nd call for participation for the First Syntax-Guided Synthesis
Competition <http://www.sygus.org/> to be organized as a satellite event of
SYNT <http://vsl2014.at/meetings/SYNT-index.html>/CAV<http://cavconference.org/>and
as part of FLoC
Olympic Games 2014 <http://vsl2014.at/olympics/> at Vienna Summer of
Logic<http://vsl2014.at> (VSL).
VSL will consist of twelve large conferences and numerous workshops,
attracting an expected number of 2500 researchers from all over the world.

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 (MIT) and Armando Solar-Lezama (MIT). For questions
regarding the competition please contact the organizers at
sygus-organizers at seas.upenn.edu.

Categories

In the first year of the competition, we will have a single track. The
solvers are expected to support the complete SyGuS-IF
format<https://github.com/rishabhs/sygus-comp14/blob/master/docs/sygus-language.pdf?raw=true>for
the theories of bit-vector and integer linear arithmetic. However,
participants can still submit their tools even if the “let” construct in
the grammars is not supported. Solvers that don’t support the “let”
construct would be evaluated against similar solvers.

Benchmarks for the competition

We will evaluate the solvers on a subset of public
benchmarks<https://github.com/rishabhs/sygus-comp14/tree/master/benchmarks>and
some secret benchmarks. The benchmarks domain areas include bit-vector
manipulation, including bit-vector algorithms, concurrency, robotics, and
invariant generation.

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.

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.

Important Dates:

Solver Submission Deadline: 15 June 2014

Competition takes place: 28 June 2014

Results published: 10 July 2014

Awards: 21 July 2014 at the FLoC Awards Ceremony<http://vsl2014.at/olympics/>

Solver Presentations: 23-24 July 2014 (with
SYNT<http://vsl2014.at/meetings/SYNT-index.html>
)

Awards

The winner(s) of the competition will be awarded Olympic Games certificates
(one per team member) and Kurt Goedel
medals<http://www.muenzeoesterreich.at/eng/medaillen/highlights.> made
of silver (one per team) in a ceremony of the FLoC Olympic Games
2014<http://vsl2014.at/olympics/>.
 In addition the winner(s) will also receive $1000, sponsored
graciously by Microsoft
Research <http://research.microsoft.com/en-us/>.

===========================

Overall Vienna Summer of Logic 2014 announcement is available here: VSL’s
announcement<http://vsl2014.at/Vienna_Summer_of_Logic_2014_Announcement.txt>
.

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