Aim and Scope

Concurrent systems are notoriously hard to design, implement, and verify. Formal synthesis has been investigated in various contexts, but had limited success in practice. The increasing importance of concurrent systems, and the inherent difficulty in verifying them postfactum, provide an exciting practical setting for investigation of formal synthesis.

The aim of this workshop is to bring together researchers to exchange and develop new ideas in all aspects of formal program synthesis, with emphasis on concurrent systems. We invite contributions from a wide spectrum of areas, ranging from basic theory to applied practical work.

Interested in Synthesis? Consider applying to the
2011 Summer School on Program Synthesis, August 8-12, 2011

Speakers

9:00-10:00Rajeev AlurComputer Augmented Program Engineering[slides]
10:00-10:30Coffee Break
10:30-11:00Roderick BloemController Synthesis Using Uninterpreted Functions
11:00-11:30Bernd FinkbeinerBounded Synthesis
11:30-12:00Peter HawkinsConcurrent Data Representation Synthesis
12:00-13:30Lunch
13:30-14:00Viktor KuncakTowards Implicit Programming[slides]
14:00-14:30Doug SmithSynthesis of Concurrent Garbage Collectors[slides]
14:30-15:00Armando Solar-LezamaConstraint based synthesis from sketches to storyboards and beyond
15:00-15:30Coffee Break

Abstracts

Computer Augmented Program Engineering
Rajeev Alur, University of Pennsylvania,
http://www.cis.upenn.edu/~alur/

In classical synthesis, an optimizing compiler transforms a high-level specification into a lower-level implementation. In the more recent view, the synthesis tool assists the programmer in various programming tasks by integrating a variety of specifications using a mix of computational tools. In this talk, we will review the recent progress in this emerging methodology, called "computer augmented program engineering". As a specific example, we will show how synthesizing the inverse of canonicalization routines for data structures can be effectively used in revealing representation dependence bugs in open source image-formatting software.

Controller Synthesis Using Uninterpreted Functions
Roderick Bloem, Graz University,
http://www.iaik.tugraz.at/content/about_iaik/people/bloem_roderick/

Data paths are easy to program and hard to specify. Concurrency requirements are hard to program but often simple to specify. Thus, synthesis should be expected to be most beneficial in providing a concurrency framework for an existing data path, where the data path should be abstracted heavily. We show one example of such an application by extending the Bucrch/Dill paradigm for pipeline verification to pipeline synthesis, using uninterpreted functions to abstract the data path.

Bounded Synthesis
Bernd Finkbeiner, Universitat des Saarlandes
http://react.cs.uni-sb.de/finkbeiner

A fundamental challenge in the synthesis of reactive systems is the size of the search space: the number of candidate implementations of a temporal specification is typically superexponential or even, for distributed system architectures, infinite. In this talk, I will review the bounded synthesis approach, which makes it possible to traverse this immense search space in a structured manner. We fix a bound on a system parameter, such as the number of states, and limit the search to those implementations that fall below the bound. By incrementally expanding the search to larger bounds, we maintain completeness, while orienting the search towards the simplest (and often most useful) solutions. The approach is applicable to the entire range of synthesis problems, from individual processes to synchronous and asynchronous distributed systems, to systems with additional design constraints, such as symmetry. The talk is based on joint work with Sven Schewe.

Synthesis of Concurrent Garbage Collectors
Doug Smith, Kestrel Institute
http://www.kestrel.edu/home/people/smith/

We generate concurrent garbage collectors by an automated refinement process in Kestrel's Specware system. Starting from a formal specification of requirements, we apply a sequence of transformations that generate correct-by-construction refinements, resulting in the generation of efficient compilable code. To handle the specification and refinement of stateful/concurrent processes, we developed techniques for a mixed algebraic/coalgebraic-style of specification within the higher-order logic of Specware's MetaSlang language. In addition to generic techniques for algorithm design, we developed new coalgebraically-oriented techniques for invariant maintenance and refining the types of observers. We generate refinements using purely functional calculation based on the axioms and theorems of the domain specification. As a final step, we transform the coalgebraic operators to stateful form and encapsulate the top-level processes as threads.

Constraint based synthesis from sketches to storyboards and beyond
Armando Solar-Lezama,MIT
http://people.csail.mit.edu/asolar/

Synthesis approaches based on constraint solving offer some unique opportunities to experiment with more natural and more interactive forms of collaboration between programmers and synthesis engines. This talk will describe how constraint based synthesis technology can enable a multi-modal programming model, where programmers can combine insights in different forms ranging from low-level insights about the structure of the desired program to high-level graphical intuitions about how the program modifies its state. The talk will elaborate on some of the technical challenges involved in making new forms of interaction possible, as well as some of the open problems behind this technology.

Concurrent Data Representation Synthesis
Peter Hawkins, Stanford
http://theory.stanford.edu/~hawkinsp/

We consider the problem of specifying combinations of concurrent data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract concurrent data types are specified using relational algebra and functional dependencies. We describe (1) a language of decompositions that permit the user to specify different combinations of data structures to represent a relation, and (2) a language of lock placements that allow the user to specify a range of conservative and speculative locking strategies at a variety of granularities. We show that given a decomposition and a lock placement, a compiler can generate serializable transactions that operate over decomposed relations. Finally we describe an autotuner that can simultaneously explore the space of decompositions and lock placements to synthesize an optimal combination of data structures and locks.

Towards Implicit Programming
Viktor Kuncak, EPFL
http://lara.epfl.ch/~kuncak/

We argue for a programming model where automated reasoning plays a key role during (1) interactive program development, (2) program compilation, and (3) program execution. I will focus on data manipulation (as opposed to control). I outline our results in complete functional synthesis for integer arithmetic, which is a form of program compilation based on decision procedures. For program development, I sketch our ongoing work on resolution theorem proving for interactive synthesis. For program execution, I touch upon the UDITA system based on Java Pathfinder, and argue that programming models related to constraint logic programming should play a bigger role in mainstream software. For more information, please see: http://lara.epfl.ch/w/impro

Sponsors

IBM Research