Preface

Software synthesis is rapidly developing into an important research area with vast potential for practical application. The SYNT Workshop on Synthesis aims to bringing together researchers interested in synthesis to present both ongoing and mature work on all aspects of automated synthesis and its applications.

The second iteration of SYNT took place in Saint Petersburg, Russia, and was co-located with the 25th International Conference on Computer Aided Verification. The workshop included eleven presentations covering the full scope of the emerging synthesis community, as well as a discussion lead by Swen Jacobs on the organization of two new synthesis competitions focusing on reactive synthesis and syntax-guided functional synthesis respectively.

Our thanks go to the authors and the speakers for their contributions to the workshop.

The invited talks were by the following speakers:

Ruzica Piskac: Software Synthesis using Automated Reasoning

Yih-Kuen Tsay: Playing Games with GOAL and Büchi Store (work with Ming-Hsien Tsai)

Rohit Singh: Synthesis of formula optimizers for Synthesizers and SMT Solvers

Franck Cassez: Efficient On-the-Fly Algorithms for Partially Observable Timed Games

Roderick Bloem: Synthesizing Boolean Controllers for Systems with Uninterpreted Functions

Swen Jacobs: The Synthesis Competition

The contributed presentations were on the following work:

Eric Wolff, Ufuk Topcu and Richard Murray: Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic

Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci: Control Software Synthesis from System Level Formal Specifications

Rishabh Singh, Sumit Gulwani and Armando Solar-Lezama: Using Synthesis for Automated Feedback Generation for Programming Assignments

Andrew Noyes, Todd Warszawski, Pavol Cerny and Nate Foster: Toward Synthesis of Network Updates (Regular paper)

Rastislav Bodik and Emina Torlak: Growing Solver-Aided Languages with Rosette

The program was put together by the two co-chairs with the support of the program committee which thorougly reviewed all the submissions for invited talks, contributed talks without publication and regular papers.

 
Finally, we would like to thank the organizers of CAV 2013 for their support in the organization of this workshop, as well as  the NSF funded ExCape project, the Austrian Society for Rigorous Software Engineering and the Transregional Collaborative Research Center 14 AVACS for their sponsorship of the workshop.

Bernd Finkbeiner and Armando Solar-Lezama

Software Synthesis using Automated Reasoning

Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier while increasing both the productivity of the programmer and the correctness of the produced code. In this talk I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First I will describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. I will illustrate the process of turning a decision procedure into a synthesis procedure using linear integer arithmetic as an example. In addition, I will outline a procedure that synthesizes code snippets from specifications implicitly given in the form of type constraints. As there can be multiple solutions, more than one code snippet can be a good candidate. We use an additional weight function to rank the derived snippets and direct the search for them. In practical evaluation, our technique scales to programs with thousands of visible declarations in scope and succeeds in 0.5 seconds to suggest program expressions of interest.

Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic

We develop a framework for optimal control policy synthesis for non-deterministic transition systems subject to temporal logic specifications. We use a fragment of temporal logic to specify tasks such as safe navigation, response to the environment, persistence, and surveillance. By restricting specifications to this fragment, we avoid a potentially doubly-exponential automaton construction. We compute feasible control policies for non-deterministic transition systems in time polynomial in the size of the system and specification. We also compute optimal control policies for average, minimax (bottleneck), and average cost-per-task-cycle cost functions. We highlight several interesting cases when these can be computed in time polynomial in the size of the system and specification. Additionally, we make connections between computing optimal control policies for an average cost-per-task-cycle cost function and the generalized traveling salesman problem. We give simulation results for motion planning problems.

Control Software Synthesis from System Level Formal Specifications

Many control systems are indeed Software Based Control Systems (SBCS), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of correct-by-construction control software.

We present algorithms and tools (namely, QKS) that from a Discrete Time Linear Hybrid System (DTLHS) model of the controlled system (the plant), Implementation Specifications (that is, number of bits in the Analog-to-Digital, AD, conversion) and System Level Formal Specifications (that is, safety and liveness requirements for the closed loop system) return correct-by-construction control software whose Worst Case Execution Time (WCET) is at most linear in the number of AD bits (this is important since typically a SBCS is a hard real-time system).

We model the plant as well as safety and liveness properties as Boolean combinations of linear constraints over real as well as discrete variables. We use a Mixed Integer Linear Programming (MILP) solver (namely, GLPK), to explicitely compute a suitable finite state automaton overapproximating the plant behaviour and use Ordered Binary Decision Diagrams (OBDDs) to compute a controller meeting the given specifications and to generate a C implementation for such a controller.

We present experimental results on using the above approach to synthesize control software for classical challenging examples: the buck DC-DC converter (a widely used mixed-mode analog circuit) and the inverted pendolum.

Using Synthesis for Automated Feedback Generation for Programming Assignments

We are currently witnessing a big paradigm shift in the landscape of online education with the advent of Massive Open Online Courses (MOOC). MOOCs enable accessibility of quality education to hundreds of thousands of students worldwide, but the dramatic increase in the size of the classrooms (from few hundreds in the traditional setting to several hundred thousands in the online setting) also presents a lot of interesting challenges to maintain a similar education standard. Some of these challenges include providing personalized feedback for assignment problems, generating new problems of different complexity levels, and providing hints for solving problems. In this talk, we consider the problem of providing automated feedback for introductory programming problems.

Growing Solver-Aided Languages with Rosette

SAT and SMT solvers have automated a spectrum of programming tasks, including program synthesis, code checking, bug localization, program repair, and programming with oracles. In principle, we obtain all these benefits by translating the program (once) to a constraint system understood by the solver. In practice, however, compiling a language to logical formulas is a tricky process, complicated by having to map the solution back to the program level and extend the language with new solver-aided constructs, such as symbolic holes used in synthesis.

This paper introduces Rosette, a framework for designing solver-aided languages. Rosette is realized as a solver-aided language embedded in Racket, from which it inherits extensive support for meta-programming. Our framework frees designers from having to compile their languages to constraints: new languages, and their solver-aided constructs, are defined by shallow (library-based) or deep (interpreter-based) embedding in Rosette itself.

We describe three case studies, by ourselves and others, of using Rosette to implement languages and synthesizers for web scraping, spatial programming, and superoptimization of bitvector programs.

Playing Games with GOAL and Büchi Store

Infinite two-player games provide an intuitive framework for modeling the interaction between a reactive system and its environment. Their formulation and solution have thus constituted a natural, prominent approach to the automatic synthesis of reactive systems. Among the various kinds of games considered by researchers, parity games (on finite graphs) have attracted most attention for conceptual simplicity, expressiveness, and possibility of relatively efficient solutions. Whether parity games can be solved in polynomial time also poses a challenging open problem. In this presentation, we give a tutorial exposition of two tools, namely GOAL and Büchi Store that may assist the user in understanding the fundamentals of infinite two-player games, particularly parity games.¹ The tools are also useful for conducting comparative studies on algorithms for solving games.

GOAL provides comprehensive support for visually defining and manipulating ω-automata and games, including parity games, while Büchi Store is an open, expanding Web-based repository of ω-automata corresponding to temporal properties of common patterns. One may define a parity game in GOAL by drawing the game graph directly or by converting some ω-automaton, which in turn may be obtained by translation from a temporal formula using GOAL or downloading from Büchi Store. Many well-known algorithms for solving parity games have been implemented in GOAL. Most of the algorithms may be performed step by step, with the intermediate results illustrated graphically and textually. This feature should be helpful for understanding how these algorithms work. GOAL also supports reachability and Büchi games.

^{1. GOAL is available at http://goal.im.ntu.edu.tw and Büchi Store at http://buchi.im.ntu.edu.tw.}

Synthesis of formula optimizers for Synthesizers and SMT Solvers

I will present a new Machine Learning and Synthesis based approach to automatically generate optimization rules to simplify a set of constraints before passing them to a solver. Such optimization rules are an integral part of modern synthesis and verification engines, and are difficult to write because in addition to being performance critical, they can introduce subtle bugs into a system when coded incorrectly. Moreover, different domains often require different optimizations, which makes for a difficult balancing act between efficiency and maintainability. In this work, we use a corpus of constraints from problems in a given domain to identify common patterns that may be amenable to optimization. We use the Sketch synthesis tool to generate valid rewrite rules for these sub-problems, and we then compile this rules into a formula simplification module that can be incorporated into the solver. We are currently targeting the solver used by the Sketch synthesizer itself, but the technique is very general and can be applied to other tools which emplot SAT/SMT solvers as their backends and traditionally have handcrafted rewrite rules in the tool which are suitable to their domain.