Published: 28th March 2014 DOI: 10.4204/EPTCS.142 ISSN: 2075-2180 |
Preface Bernd Finkbeiner and Armando Solar-Lezama | |
Invited Presentation:
Software Synthesis using Automated Reasoning Ruzica Piskac | 1 |
Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic Eric M. Wolff, Ufuk Topcu and Richard M. Murray | 2 |
Control Software Synthesis from System Level Formal Specifications Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci | 3 |
Using Synthesis for Automated Feedback Generation for Programming Assignments Rishabh Singh, Sumit Gulwani and Armando Solar-Lezama | 4 |
Growing Solver-Aided Languages with Rosette Rastislav Bodik and Emina Torlak | 5 |
Invited Presentation:
Playing Games with GOAL and Büchi Store Ming-Hsien Tsai and Yih-Kuen Tsay | 6 |
Invited Presentation:
Synthesis of formula optimizers for Synthesizers and SMT Solvers Rohit Singh | 7 |
Toward Synthesis of Network Updates Andrew Noyes, Todd Warszawski, Pavol Černý and Nate Foster | 8 |
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.
Roderick Bloem | Graz University of Technology |
Rastislav Bodik | UC Berkeley |
Swarat Chaudhuri | Rice University |
Bernd Finkbeiner (co-chair) | Saarland University |
Barbara Jobstmann | CNRS, Verimag and Jasper DA |
Orna Kupferman | Hebrew University |
Doron Peled | Bar Ilan University |
Nir Piterman | University of Leicester |
Sven Schewe | University of Liverpool |
Armando Solar-Lezama (co-chair) | MIT |
Martin Vechev | ETH Zurich |
Eran Yahav | Technion |
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 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.
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.
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.
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.
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.
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.^{1}
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.}
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.