Published: 22nd November 2016|
|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|
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
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/.
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.