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,

• Bernd Finkbeiner, Saarland University,
• Viktor Kuncak, EPFL,
• Leonid Ryzhyk, University of Toronto, and
• Ashish Tiwari, SRI International

• Pavol Cerny, University of Colorado at Boulder
• Krishnendu Chatterjee, IST Austria
• Rüdiger Ehlers, University of Bremen / DFKI
• Bernd Finkbeiner, Saarland University
• Swen Jacobs, TU Graz
• Susmit Jha, Intel Strategic CAD Lab
• Barbara Jobstmann, Jasper Design Automation / EPFL
• Orna Kupferman, Hebrew University of Jerusalem
• Nir Piterman, University of Leicester
• Jean-François Raskin, Université libre de Bruxelles
• Sriram Sankaranarayanan, University of Colorado
• Armando Solar-Lezama, Massachusetts Institute of Technology
• Ashish Tiwari, SRI International
• Emina Torlak, UC Berkeley

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

Automating Deductive Synthesis with Leon

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

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

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

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.