Published: 18th July 2014
DOI: 10.4204/EPTCS.157
ISSN: 2075-2180

EPTCS 157

Proceedings 3rd Workshop on
Synthesis
Vienna, Austria, July 23-24, 2014

Edited by: Krishnendu Chatterjee, Rüdiger Ehlers and Susmit Jha

Preface
Krishnendu Chatterjee, Rüdiger Ehlers and Susmit Jha
Invited Talk: Automating Deductive Synthesis with Leon
Viktor Kuncak
1
Invited Talk: Synthesis using EF-SMT Solvers
Ashish Tiwari
2
Invited Talk: Automatic Device Driver Synthesis Project: a Work-in-Progress Report
Leonid Ryzhyk
3
Invited Talk: Petri Games: Synthesis of Distributed Systems with Causal Memory
Bernd Finkbeiner
4
Synthesis of a simple self-stabilizing system
Adrià Gascón and Ashish Tiwari
5
Program Synthesis and Linear Operator Semantics
Herbert Wiklicky
17
How to Handle Assumptions in Synthesis
Roderick Bloem, Rüdiger Ehlers, Swen Jacobs and Robert Könighofer
34
Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Aaron Bohy, Véronique Bruyère and Jean-François Raskin
51
Parameterized Synthesis Case Study: AMBA AHB
Roderick Bloem, Swen Jacobs and Ayrat Khalimov
68
Are There Good Mistakes? A Theoretical Analysis of CEGIS
Susmit Jha and Sanjit A. Seshia
84
AbsSynthe: abstract synthesis from succinct safety specifications
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin and Ocan Sankur
100
Low-Effort Specification Debugging and Analysis
Rüdiger Ehlers and Vasumathi Raman
117

Preface

The idea of synthesis, i.e., the process of automatically computing implementations from their specifications, has recently gained a lot of momentum in the contexts of software engineering and reactive system design. While it is widely believed that, due to complexity/undecidability issues, synthesis cannot completely replace manual engineering, it can assist the process of designing the intricate pieces of code that most programmers find challenging, or help with orchestrating tasks in reactive environments.

The Third Workshop on Synthesis (SYNT 2014) aimed at bringing together and providing an open platform for researchers interested in synthesis. Research on synthesis exists well alongside conferences on formal methods and verification, such as CAV, which aim at improving the reliability of systems. Driven by the vast potential for practical applications of synthesis, its goal was to foster scientific exchange not only within the areas of software and reactive synthesis, but also between them. The workshop was co-located with the 26th International Conference on Computer Aided Verification (CAV) and took place at July 23th and 24th 2014 in the scope of the Vienna Summer of Logic 2014 in Vienna, Austria.

The workshop consisted of four invited talks, eight contributed talks with regular papers, and two synthesis competition reports. We thank the invited speakers,

for their commitment and contribution. Furthermore, we thank Raveej Alur and Swen Jacobs for their presentations on the results of the First Syntax-Guided Synthesis Competition (SyGuS) and the First Synthesis Competition for Reactive Systems (SyntComp), respectively.

The selected papers and contributed talks have emerged from a thorough reviewing process with three to four reviews per paper. Our special thanks go to the SYNT 2014 program committee: We would also like to thank our external referee Adria Gascon for contributing to the reviewing process.

Finally, we would like to thank the organizers of CAV 2014 for their support in the organization of this workshop, as well as the NSF funded Expedition in Computer Augmented Program Engineering (ExCAPE) project and the Austrian Rigorous System Engineering Network (RiSE) for their sponsorship of the workshop.

July 2014, Krishnendu Chatterjee, Rüdiger Ehlers, and Susmit Jha


Automating Deductive Synthesis with Leon

Viktor Kuncak (EPFL)

Software verification is next to impossible, and synthesis appears harder. However, transforming one specification into another can sometimes be easier than showing that two versions of the specification are equivalent. We thus believe that semi-automatic transformations of specifications are a promising way of constructing software with strong correctness properties. We present our current deployment of synthesis based on transformation of specification, in the system http://leon.epfl.ch. This implementation subsumes synthesis procedures, but is not limited to decidable logics, and also incorporates two counterexample-guided synthesis algorithms. We have used it to automatically construct pure recursive functions operating on unbounded data structures.


Synthesis using EF-SMT Solvers

Ashish Tiwari (SRI International)

Satisfiability modulo theory (SMT) solvers check satisfiability of Boolean combination of formulas that contain symbols from several different theories. All variables are (implicitly) existentially quantified. Exists-forall satisfiability modulo theory (EF-SMT) solvers check satisfiability of formulas that have a exists-forall quantifier prefix. Just as SMT solvers are used as backend engines for verification tools (such as, infinite bounded model checkers and k-induction provers), EF-SMT solvers are potential backends for synthesis tools. This talk will describe the EF-extension of the Yices SMT solver and present results on using it for reverse engineering hardware.


Automatic Device Driver Synthesis Project: a Work-in-Progress Report

Leonid Ryzhyk (University of Toronto)

Automatic device driver synthesis is one of the first real-world applications of the reactive synthesis technology to date. This talk will give an overview of an ongoing three-year project funded by Intel, aiming to develop a suite of practical device driver synthesis tools. The project is pursued jointly by researchers from the University of Toronto, University of Colorado Boulder, Imperial College London, NICTA, and IST Austria. The talk will present the key contributions made by the project so far, as well as the main remaining challenges. In particular, I will describe the first practical abstraction-refinement algorithm for games and a user-guided synthesis methodology, which combines the power of automation with the flexibility of conventional development. I will give a demo of our synthesis tool, showing its support for interactive code generation and efficient troubleshooting of synthesis failures using counterexample-guided debugging.


Petri Games: Synthesis of Distributed Systems with Causal Memory

Bernd Finkbeiner (Saarland University)

We introduce Petri games as a new foundation for the synthesis of distributed systems. The players of a Petri game consist of the system processes and the external environment, all represented as tokens on a Petri net. The players memorize their causal history and communicate it to each other during each synchronization. Petri games lead to new decidability results and algorithms for the synthesis of distributed systems.
Joint work with Ernst-Rüdiger Olderog.