ABSTRACT. Automatic device driver synthesis is one of the first real-world applications of the reactive synthesis technology to date. This talk will give an overview of an ongoing three-year project funded by Intel, aiming to develop a suite of practical device driver synthesis tools. The project is pursued jointly by researchers from the University of Toronto, University of Colorado Boulder, Imperial College London, NICTA, and IST Austria. The talk will present the key contributions made by the project so far, as well as the main remaining challenges. In particular, I will describe the first practical abstraction-refinement algorithm for games and a user-guided synthesis methodology, which combines the power of automation with the flexibility of conventional development. I will give a demo of our synthesis tool, showing its support for interactive code generation and efficient troubleshooting of synthesis failures using counterexample-guided debugging.

ABSTRACT. We revisit the AMBA AHB case study that has been a benchmark for reactive synthesis tools for a long time. Synthesizing AMBA AHB implementations that can serve a large number of masters is still a difficult problem. We demonstrate how to use parameterized synthesis in token rings to obtain an implementation for a component that serves a single master, and can be arranged in a ring of arbitrarily many components. We describe new tricks -- property decompositional synthesis, and direct encoding of simple GR1 -- that together with previously described optimizations allowed us to synthesize the model with 14 states in 1 hour.

ABSTRACT. Counterexample-guided inductive synthesis (CEGIS) is used to synthesize programs from a candidate space of programs. The technique is guaranteed to terminate and synthesize the correct program if the space of candidate programs is finite. But the technique may or may not terminate with the correct program if the candidate space of programs is infinite. In this paper, we perform a theoretical analysis of counterexample-guided inductive synthesis technique. We investigate whether the set of candidate spaces for which the correct program can be synthesized using CEGIS depends on the counterexamples used in inductive synthesis, that is, whether there are good mistakes which would increase the synthesis power. We investigate whether the use of minimal counterexamples instead of arbitrary counterexamples expands the set of candidate spaces of programs for which inductive synthesis can successfully synthesize a correct program. We consider two kinds of counterexamples: minimal counterexamples and history bounded counterexamples. The history bounded counterexample used in any iteration of CEGIS is bounded by the examples used in previous iterations of inductive synthesis. We examine the relative change in power of inductive synthesis in both cases. We show that the synthesis technique using minimal counterexamples MinCEGIS has the same synthesis power as CEGIS but the synthesis technique using history bounded counterexamples HCEGIS has different power than that of CEGIS.

ABSTRACT. We introduce Petri games as a new foundation for the synthesis of distributed systems. The players of a Petri game consist of the system processes and the external environment, all represented as tokens on a Petri net. The players memorize their causal history and communicate it to each other during each synchronization. Petri games lead to new decidability results and algorithms for the synthesis of distributed systems. Joint work with Ernst-Ruediger Olderog.

ABSTRACT. In this paper, we describe a synthesis algorithm for safety specifications described as circuits. Our algorithm is based on fixpoint computations, abstraction and refinement, it uses binary decision diagrams as symbolic data structure. We evaluate our tool on the benchmarks provided by the organizers of the synthesis competition organized within the SYNT’14 workshop.

ABSTRACT. In reactive synthesis, we automatically construct implementations for reactive systems from their specifications. To make the approach feasible in practice, a system engineer needs to have effective and efficient means to debug a specification.

In this paper, we provide techniques for report-based specification debugging, where a specification's properties are analyzed and the result is presented to the user as report. This provides a low-effort way to debug specifications and complements simulating a synthesized implementation as a more high-effort technique. We show the usefulness of our report-based specification debugging tool set by providing examples in the context of generalized reactivity(1) synthesis.