A natural progress from checking the correctness of code is to synthesize software from its formal specification. While it is widely believed that, due to complexity/undecidability issues, software synthesis cannot completely replace programmers, it can still assist the process of designing the intricate pieces of code that most programmers find challenging.

Synthesis has recently progressed substantially and is starting to become a viable research area with vast potential for practical applications. This kind of research exists well alongside conferences on formal methods and verification, such as CAV, which aim at improving the reliability of systems.
This workshop aims at bringing together and providing an open platform for researchers interested in synthesis.


Saturday, July 13

9:25-9:30 Opening
9:30-10:30 Software Synthesis using Automated Reasoning (Ruzica Piskac)
10:30-11:00 Coffee break
11:00-11:45 Growing Solver-Aided Languages with Rosette (Rastislav Bodik and Emina Torlak)
11:45-12:30 Control Software Synthesis from System Level Formal Specifications (Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci)
12:30-2:00 Lunch break
2:00-2:45 Using Synthesis for Automated Feedback Generation for Programming Assignments (Rishabh Singh, Sumit Gulwani and Armando Solar-Lezama)
2:45-3:30 Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic (Eric Wolff, Ufuk Topcu and Richard Murray)
3:30-4:00 Coffee break
4:00-5:00 Playing Games with GOAL and Büchi Store (M.-H. Tsai and Yih-Kuen Tsay)

Sunday, July 14

9:30-10:30 Synthesis of formula optimizers for Synthesizers and SMT Solvers (Rohit Singh)
10:30-11:00 Coffee break
11:00-12:00 Efficient On-the-Fly Algorithms for Partially Observable Timed Games (Franck Cassez)
12:00-1:45 Lunch break
1:45-2:45 Synthesizing Boolean Controllers for Systems with Uninterpreted Functions (Roderick Bloem)
2:45-3:30 Toward Synthesis of Network Updates (Andrew Noyes, Todd Warszawski, Pavol Cerny and Nate Foster)
3:30-4:00 Coffee break
4:00-5:00 Presentation and Discussion: The Synthesis Competition (Swen Jacobs)

Invited Speakers

Roderick Bloem Graz University of Technology
Franck Cassez National ICT Australia
Swen Jacobs Graz University of Technology
Ruzica Piskac Max Planck Institute for Software Systems
Rohit Singh MIT
Yih-Kuen Tsay National Taiwan University

Contributed Presentations

Topics of Interest

Topics of interest include, but are not limited to:

Proceedings & Submission Guidelines

We accept

Submitted regular and tool papers must be original and unpublished. Regular and tool papers accepted for presentation at the workshop will appear in the Electronic Proceedings in Theoretical Computer Science series; hence, submissions must be prepared in LaTeX using the EPTCS macro package. Submission accepted for presentation must be presented at the workshop by at least one of the authors.
Extended versions of selected papers (including presentations) will appear in a special issue of Acta Informatica.

Authors should submit PDF files of their papers and manuscripts through EasyChair.

Important Dates:

Paper submission: April 26, 2013
Notification: May 26, 2013
Camera ready version: June 21th, 2013
Workshop: July 13th and 14th, 2013
We kindly ask submission authors and potential participants to apply for a visa invitation letter as soon as possible (even if their trip plans may change later). For further details please check: http://cav2013.forsyte.at/visa/

Programme Committee

Roderick Bloem Graz University of Technology
Rastislav Bodik UC Berkeley
Swarat Chaudhuri Rice University
Bernd Finkbeiner (co-chair) Saarland University
Barbara Jobstmann CNRS, Verimag and Jasper DA
Orna Kupferman Hebrew University
Doron Peled Bar Ilan University
Nir Piterman University of Leicester
Sven Schewe University of Liverpool
Armando Solar-Lezama (co-chair) MIT
Martin Vechev ETH Zurich
Eran Yahav Technion

SYNT 2013 is supported by

AVACS ExCAPE RiSE