Preface

• Rastislav Bodik,
• Bernd Finkbeiner,
• Madhusudan Parthasaraty,
• Paulo Tabuada, and
• Farn Wang,

• Nathalie Bertrand INRIA Rennes, France
• Rastislav Bodik UC Berkeley, USA
• Bernd Finkbeiner Univesrität des Saarlandes, Germany
• Orna Kupferman Hebrew University, Israel
• Oded Maler CNRS VERIMAG, France
• Doron Peled Bar Ilan University, Israel
• Nir Piterman University of Leicester, UK
• Sven Schewe University of Liverpool, UK
• Martin Vechev ETH Zürich, Switzerland
• Eran Yahav Technion, Israel
• Lijun Zhang Technical University of Denmark

• Ayrat Khalimov, Swen Jacobs and Roderick Bloem (Towards Efficient Parameterized Synthesis),
• Alin Stefanescu (Synthesis of synchronous products and asynchronous automata: from theory to practice),
• Jasen Markovski (A Synthesis-Based Framework for Systems Engineering), and
• Scott C. Livingston, Pavithra Prabhakar and Richard M. Murray (A method for patching control strategies based on local mu-calculus fixed points).

Synthesis for Systems Biology

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

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

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

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

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.