Published: 22nd November 2016
DOI: 10.4204/EPTCS.229
ISSN: 2075-2180

EPTCS 229

Proceedings Fifth Workshop on
Synthesis
Toronto, Canada, July 17-18, 2016

Edited by: Ruzica Piskac and Rayna Dimitrova

Preface
Rayna Dimitrova and Ruzica Piskac
Invited Talk: From Linear Systems to Discrete-Event Systems
W. Murray Wonham
1
Invited Talk: Synthesizing Event-driven Network Programs from Scenarios
Pavol Černý
2
Using SyGuS to Synthesize Reactive Motion Plans
Sarah Chasins and Julie L. Newcomb
3
What You Really Need To Know About Your Neighbor
Werner Damm, Bernd Finkbeiner and Astrid Rakow
21
Symbolic BDD and ADD Algorithms for Energy Games
Shahar Maoz, Or Pistiner and Jan Oliver Ringert
35
Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions
Grigory Fedyukovich and Rastislav Bodík
55
Leveraging Parallel Data Processing Frameworks with Verified Lifting
Maaz Bin Safeer Ahmad and Alvin Cheung
67
Developing a Practical Reactive Synthesis Tool: Experience and Lessons Learned
Leonid Ryzhyk and Adam Walker
84
An Update on Deductive Synthesis and Repair in the Leon Tool
Manos Koukoutos, Etienne Kneuss and Viktor Kuncak
100
A High-Level LTL Synthesis Format: TLSF v1.1
Swen Jacobs, Felix Klein and Sebastian Schirmer
112
The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond
Swen Jacobs and Roderick Bloem
133
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup and Adam Walker
149
SyGuS-Comp 2016: Results and Analysis
Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama
178

Preface

The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyberphysical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in particular application domains is encouraged.

The fifth iteration of the workshop took place in Toronto, Canada. It was co-located with the 28th International Conference on Computer Aided Verification. The workshop included twelve contributed talks and two invited talks. In addition, it featured a special session about the Syntax-Guided Synthesis Competition (SyGuS) and the SyntComp Synthesis competition.

The workshop consisted of two invited talks, twelve contributed talks, among which eight regular papers, one tool paper and three presentation-only submissions, and two synthesis competition reports. We thank the invited speakers, W. Murray Wonham and Pavol Černý. Furthermore, we thank Dana Fisman and Swen Jacobs for their presentations on the results of the Syntax-Guided Synthesis Competition (SyGuS) and the 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 thanks go to the SYNT 2016 program committee:

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

Rayna Dimitrova, Ruzica Piskac


From Linear Systems to Discrete-Event Systems

W. Murray Wonham (University of Toronto)

In this talk we trace the development of a control theory of discrete-event systems (DES), first proposed around 1983 and currently an active area of research. The general concepts underlying modern control theories - stability, optimality, controllability, and observability - had evolved throughout the 1940s-'60s, notably in the approaches to linear system synthesis pioneered by Wiener, Krasovskii, Kalman and others. Perhaps surprisingly, the adaptation of these concepts to the seemingly quite different setting appropriate to DES - automata and formal languages - proved to be relatively straightforward, especially on the analogy of ideas from geometric linear control (like subspace ordering) that had emerged in the 1960s and '70s.

Until fairly recently, the application of DES control theory to problems of realistic industrial size has been inhibited by exponential state-space explosion. We can now, however, report success in confronting exponentiality through effective control architecture - for instance an adaptation of state charts - combined with symbolic computing techniques involving binary or integer decision diagrams. In these approaches it is often useful to identify 'natural' system structure as the point of departure, while a continuing challenge is how to 'steer' a formal synthesis towards a common-sense simple and comprehensible solution when the latter happens to exist. More generally, the long term goal is to identify the "laws of control architecture."

Background material for this talk is posted at: http://www.control.utoronto.ca/DES/.

Synthesizing Event-driven Network Programs from Scenarios

Pavol Černý (University of Colorado Boulder)

Although Software-Defined Networking (SDN) has benefited from recent advances in programming languages and verification technology, there are several issues which continue to make correct network programs difficult to write. First, if a distributed network program needs to update its (global) state in response to (local) events, consistency problems can arise, leading to misconfigurations or security vulnerabilities. Second, it is often much more difficult to reason about the full distributed program than it is to consider its individual network behaviors. To address these difficulties, we propose a new programming-by-scenarios approach for event-driven network programs.