SYNT 2013
2nd Workshop on Synthesis
July 13th and July 14th, 2013, Saint Petersburg, Russia
Co-located with the 25th International Conference on Computer Aided Verification
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
- Eric Wolff, Ufuk Topcu and Richard Murray
Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic - Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci
Control Software Synthesis from System Level Formal Specifications - Rishabh Singh, Sumit Gulwani and Armando Solar-Lezama
Using Synthesis for Automated Feedback Generation for Programming Assignments - Andrew Noyes, Todd Warszawski, Pavol Cerny and Nate Foster
Toward Synthesis of Network Updates - Rastislav Bodik and Emina Torlak
Growing Solver-Aided Languages with Rosette
Topics of Interest
Topics of interest include, but are not limited to:
- synthesis algorithms
- synthesis tools
- complexity and impossibility results for synthesis
- case studies of software or hardware synthesis
Proceedings & Submission Guidelines
We accept
- regular papers (max. 16 pages in EPTCS style),
- tool papers (max. 7 pages in EPTCS style),
- work-in-progress presentations, and
- presentations of relevant but already published work.
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.
- Manuscripts of full research papers are limited to a maximum of 16 pages (excluding technical appendices) in PDF format (EPTCS style).
- Manuscripts describing short tool papers are limited to a maximum of 7 pages in PDF (EPTCS style).
- Presentations of relevant results submitted to other forums, already published, or on not yet finished work in progress will not be considered for the final workshop proceedings, but will be considered for the special issue. Manuscripts of presentations are limited to a maximum of 10 pages.
Important Dates:
Paper submission: | April 26, 2013 |
Notification: | May 26, 2013 |
Camera ready version: | June 21th, 2013 |
Workshop: | July 13th and 14th, 2013 |
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 |