[TYPES/announce] SyGuS-COMP 2016: Call for solvers and benchmarks submissions

[Dana Fisman]

*SyGuS-COMP 2016 Call for Solvers and Benchmarks Submissions*

3rd Syntax Guided Synthesis Competition

Satellite event of CAV and SYNT 2016

*http://www.sygus.org/SyGuS-COMP2016.html
<http://www.sygus.org/SyGuS-COMP2016.html>*





*Important Dates:*



Benchmark Submission Deadline: 14 May 2016

Solver Submission Deadline: 14 June 2016

Competition Date: 28 June 2016

Results published: 14 July 2016

Solver Presentations: 17 July 2016 (at SYNT
<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fformal.epfl.ch%2fsynt%2f2016%2f&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=skGXm%2bunZQ3vqg%2bBTSvxnY4QKGftvMO9AldMzPUi%2ffI%3d>
)



*Call for Participation:*

This is a call for participation for the 3rd Syntax-Guided Synthesis
Competition
<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.sygus.org%2f&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=MbxZnc9cKZAWo0QYkmwBN5KWZN%2bqSlyAIpK3J25qCGc%3d>
to
be organized as a satellite event of SYNT
<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fformal.epfl.ch%2fsynt%2f2016%2f&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=skGXm%2bunZQ3vqg%2bBTSvxnY4QKGftvMO9AldMzPUi%2ffI%3d>
/*CAV
<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fi-cav.org%2f2016%2f&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=vGKQcMw9UZKB4hYy4gQNpZrSDlCgm5bAUQtq05hmyIQ%3d>
2016.*

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.

There has been a lot of recent interest in both using SyGuS solvers for
various synthesis applications and developing different solving algorithms.
TheSyGuS-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://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fexcape.cis.upenn.edu%2f&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=Oy6Jv%2b1oS8OjCez1g22Xdez%2f8pIwahkw%2bdaAp6Tj8rc%3d>
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**:*

This year we will be having *4* tracks. In addition to the three tracks
from last year’s competition ( 1.General SyGuS track, 2. Invariant
Synthesis track, and 3. Conditional Linear Integer Arithmetic track), we
will be having a new track: 4. Programming By Examples (PBE), where the
specification constraint would be defined using only input-output examples.
We expect to have the ICFP 2013 programming contest bitvector benchmarks
and FlashFill public benchmarks for this category. More details about the
tracks can be found in the extended SyGuS-IF
<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww.sygus.org%2ffiles%2fSyGuS-Syntax-SyGuSCOMP%2715.pdf&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=ceRNzCjNbdah5MbyZ5T13yLlXL7%2f6A6l%2fMOTuK82P68%3d>.
The results of the 2nd SyGuS competition can be found here
<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fsygus.seas.upenn.edu%2ffiles%2fSyGuSComp2015.pdf&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=u1jti%2favoCi%2fpDN0YDT9wwwgA3yi%2fdy8QsrrK3%2bGfQw%3d>
.



*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, and
invariant generation. 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
<https://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fwww.starexec.org%2fstarexec%2fpublic%2fabout.jsp&data=01%7c01%7crisin%40microsoft.com%7ca9f4489d547e4992842308d33250e45c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=wruRpNAW%2brvk27in5t4hNUU%2fjJDJZjSo3yJm7Xzhys4%3d>
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. The scoring will take into account the number of
benchmarks solved, the solving time, and the size 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.



Best regards,

Rajeev Alur (Penn), Dana Fisman (Penn), Rishabh Singh (Microsoft Research),
and Armando Solar-Lezama (MIT)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20160324/db8e1749/attachment.html>