Published: 3rd July 2012
DOI: 10.4204/EPTCS.84
ISSN: 2075-2180

EPTCS 84

Proceedings First Workshop on
Synthesis
Berkeley, California, USA, 7th and 8th July 2012

Edited by: Doron Peled and Sven Schewe

Preface
Invited Presentation: Synthesis for Systems Biology
Rastislav Bodik
Invited Presentation: Bounded Synthesis for Real-Time Systems
Bernd Finkbeiner and Hans-Jörg Peter
Invited Presentation: Synthesizing Programs using Bounded Domains and Occam's Razor
Madhusudan Parthasaraty
Invited Presentation: Synthesizing Robust Software
Paulo Tabuada, Ayca Balkan, Sina Caliskan, Yasser Shoukry and Rupak Majumdar
Invited Presentation: Consistency Checking of OpenMP Programs with TSO CPU Model
Farn Wang, Fang Yu, Shun-Ching Yang, Guan-Cheng Chen and Che-Chang Chan
Sparse Positional Strategies for Safety Games
Rüdiger Ehlers and Daniela Moldovan
1
Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs
Roopsha Samanta
17
Theory and Techniques for Synthesizing a Family of Graph Algorithms
Srinivas Nedunuri, William R. Cook and Douglas R. Smith
33
Synthesizing Robust Systems with RATSY
Roderick Bloem, Hans-Jürgen Gamauf, Georg Hofferek, Bettina Könighofer and Robert Könighofer
47

Preface

The aim of the First Workshop on Synthesis (SYNT 2012) is to bring together and provide an open platform for researchers interested in synthesis. Co-located with the 24th International Conference on Computer Aided Verification, it took place at July 7th and 8th 2012 in Berkeley, California.

A natural progress from checking the correctness of code is to synthesize software from its formal specification. While it is widely believed that, due to complexity/undecidability issues, software synthesis cannot completely replace programmers, it can still assist the process of designing the intricate pieces of code that many programmers find challenging. Synthesis has recently progressed substantially and is starting to become a viable research area with vast potential for practical applications. This kind of research exists well alongside conferences on formal methods and verification, such as CAV, which aim at improving the reliability of systems.

The workshop consists of a mix of invited talks, contributed talks (without publication), and regular papers. We thank the invited speakers, for their commitment and contribution.

The selected papers and contributed talks have emerged from a thorough reviewing process with three reviews per paper. Our special thanks to the SYNT 2012 Program Committee: We would also like to thank the external referees Hans-Jörg Peter and Thomas Varghese for their contribution.

Our thanks go to the authors of the contributed papers in these proceedings and the following authors for the presentation of their ongoing or published work: Finally, we would like to thank the organizers of CAV 2012 for their support in the organization of this workshop.

June 2012, Doron Peled and Sven Schewe

Synthesis for Systems Biology

Rastislav Bodik (University of California, Berkeley)

Cellular models constructed in executable biology are programs with well-defined semantics and thus are amenable to reasoning techniques developed for ordinary programs, such as model checking, that can confirm a model's adherence to experimental observations. I will describe our ongoing work on addressing three open questions of executable biology: (i) synthesis: automating the construction of models, which are currently constructed manually; (ii) uniqueness check: verification that a biological hypothesis encoded in a model is the sole explanation of the empirically observed cell phenomena; and, (iii) experiment suggestion: should alternative explanations exist, identification of wet-lab experiments that would disambiguate among alternative biological hypotheses plausible given observations so far.
First, I will describe how to model cell fate determination with a programming language of distributed controllers that must produce their output in bounded time. The language supports partial programs (program templates), partial traces (trace invariants), and partial specs (incomplete i/o definitions, where the input is the cell mutation and the output is the fate). The first two allow the biologist to specify her prior knowledge, while partial specs state available wet-lab experiments (mutation-fate pairs) that the model must reproduce.
To synthesize programs from these partial descriptions, we developed an inductive synthesis algorithm that reduces the search for the program into SMT constraints solving. We then build on this algorithm to determine whether provided partial descriptions are ambiguous, i.e., whether there are alternative models that would produce different cell fates on some input mutation. I will describe how we embed the modeling language in Scala and translate it into SMT constraints. As a case study, I will describe the synthesis of a model that explains vulval precursor cell (VPC) fate determination in the worm C. elegans, which is a canonical organism studied towards understanding of fate determination in higher organisms.
This presentation will describe joined work with Ali Sinan Köksal, Evan Pu, Saurabh Srivastava (UC Berkeley), Jasmin Fisher (Microsoft Research Cambridge), and Nir Piterman (University of Leicester).


Bounded Synthesis for Real-Time Systems

Bernd Finkbeiner (Universität des Saarlandes)
Hans-Jörg Peter (Universität des Saarlandes)

In bounded synthesis, we fix a bound on the size of the controller, restricting the solutions of interest to just those that meet the bound. Bounded synthesis is useful even if the size of the controller is not known in advance, because the bound can be increased incrementally, guiding the search to the minimal solutions. In this talk, we present recent results on bounded synthesis in the setting of real-time systems. We study the synthesis of timed controllers under partial observability with bounds on the discrete and timed resources of the controller. In addition to decidability and complexity results, indicating which bounds are helpful and which are useless from an algorithmic perspective, we present an effective synthesis algorithm for location-bounded discrete controllers, based on a symbolic fixed point computation.


Synthesizing Programs using Bounded Domains and Occam's Razor

Madhusudan Parthasaraty (University of Illinois at Urbana-Champaign)

We first present a technical result that shows how classical results in synthesizing transition systems against regular specifications can be extended to synthesize directly programs over bounded domains. This allows us to synthesize all programs satisfying a specification, allows us to synthesize the simplest programs satisfying a specification, and allows handling a variety of specifications including reactive LTL specifications without recourse to solving parity games. We then propose schemes that use synthesis over bounded domains in order to synthesize programs over unbounded domains, using Occam's principle and synthesizing the simplest programs for a specification. A practically viable synthesis procedure on bounded domains is hence likely to be useful for general program synthesis.


Synthesizing Robust Software

Paulo Tabuada (University of California, Los Angeles)
Ayca Balkan (University of California, Los Angeles)
Sina Caliskan (University of California, Los Angeles)
Yasser Shoukry (University of California, Los Angeles)
Rupak Majumdar (Max Planck Institute for Software Systems)

Robustness is the property that a system only exhibits small deviations from the nominal behavior upon the occurrence of small disturbances. While the importance of robustness in engineering design is well accepted, it is less clear how to verify and design discrete systems for robustness. In this talk I will present a theory of input-output (IO) stability for discrete systems inspired by existing notions in continuous control theory. I will show that IO-stability captures two intuitive goals of robustness: bounded disturbances lead to bounded deviations from nominal behavior, and the effect of a sporadic disturbance disappears in finitely many steps. For systems modeled as finite-state transducers, IO-stability can be verified and the synthesis problem can be solved in polynomial time.


Consistency Checking of OpenMP Programs with TSO CPU Model

Farn Wang (National Taiwan University)
Fang Yu (National Chengchi University)
Shun-Ching Yang (National Taiwan University)
Guan-Cheng Chen (National Taiwan University)
Che-Chang Chan (National Taiwan University)

We present a symbolic approach for checking consistency of OpenMP parallel programs. A parallel program is consistent if it yields the same result as its sequential version despite the execution order among threads. We find race conditions of an OpenMP parallel program, construct the formal models of its raced segments under relaxed memory models, and perform guided symbolic simulation to search consistency violations. The simulation terminates when (1) a witness of inconsistency has been found, or (2) all reachable states have been explored without finding an evidence of inconsistency. We have developed the tool Pathg by incorporating Omega library to solve race constraints and RED symbolic simulator to perform guided search. We show that Pathg can prove consistency of programs, identify races that modern OpenMP checkers failed to report, and find inconsistency witness effectively against benchmarks from the OpenMP Source Code Repository and the NAS Parallel benchmark suite.