Published: 18th July 2014|
|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|
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,
July 2014, Krishnendu Chatterjee, Rüdiger Ehlers, and Susmit Jha
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.
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 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.
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.