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.


Rajeev AlurGames for Formal Design and Analysis of Reactive Systems
Roderick Bloem
Bernd Finkbeiner
Peter HawkinsConcurrent Data Representation Synthesis
Viktor KuncakTowards Implicit Programming
Doug Smith
Armando Solar-LezamaConstraint based synthesis from sketches to storyboards and beyond


Games for Formal Design and Analysis of Reactive Systems
Rajeev Alur, University of Pennsylvania,

With recent advances in algorithms for state-space traversal and in techniques for automatic abstraction of source code, model checking has emerged as a key tool for analyzing and debugging software systems. This talk discusses the role of games in modeling and analysis of software systems. Games are useful in modeling open systems where the distinction among the choices controlled by different components is made explicit. We first describe the model checker Mocha that supports a game-based temporal logic for writing requirements, and its applications to analysis of multi-party security protocols. Then, we describe how to automatically extract dynamic interfaces for Java classes using predicate abstraction for extracting a boolean model from a class file, and learning algorithms for constructing the most general strategy for invoking the methods of the model. We discuss an implementation in the tool JIST---Java Interface Synthesis Tool, and demonstrate that the tool can construct interfaces, accurately and efficiently, for sample Java2SDK library classes. We will conclude with a discussion of how game-based analysis can be used to synthesize systems from their specifications.

Constraint based synthesis from sketches to storyboards and beyond
Armando Solar-Lezama,MIT

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

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

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:


IBM Research