SynthesisAugmented System Development
I am interested in
 Synthesis and repair of programs,
 Quantitative verification and synthesis (Tool: Quasy),
 Synthesis from specifications in temporal logics (Tools:
Lily,
Anzu),
 Analysis and verification of hardware designs, transactional memories, and business process models,
 Synthesis techniques for embedded systems and Interface theory, and
 Infinite games and Automata theory (Tool: GIST).
My overall goal is to simplify the development of reliable computer systems
using synthesis techniques. Synthesis techniques are promising for
several reasons.
 First, some properties of a system are much easier
stated than implemented. For instance, stating that a system should be
deadlockfree is easy, yet developing a system that is deadlockfree
can be difficult.
 Second, enforcing a property by construction is
sometimes much easier than verifying the same property a
posteriori. For instance, many invariants between two variables can be
enforced by deriving the value of one from the value of the other (a
simple example is mutual exclusion between two Boolean
variables).
 Finally, computer systems are increasingly built from
heterogeneous components, making it difficult to predict their overall
behavior and performance. As a result, designing and sizing the system
requires expert knowledge. Our novel synthesis techniques based on
quantitative constraints (discussed below) allow us to efficiently
explore the design space to find optimal tradeoffs between
conflicting design decisions.
Below I summarize the work of me and my collaborators.

Fault Localization and Repair. Motivated by the fact that debugging a
program is a very time consuming task, even if the developer is
presented with a counterexample, I have worked on automatic fault
localization and repair techniques. More precisely, we were the first
to develop and implement an approach based on game theory to
automatically localize
(FMCAD05,
DX05) and repair
(CAV05) programs. The approach
is guaranteed to produce a system that satisfies the specification. We
applied it to programs of a few hundred lines of Verilog or Clike
code (e.g., a Traffic Collision Avoidance System and a simple
DLXstyle processor, see
JCSS12 for details). Together with program
sketching (SolarLezama et al., PLDI05), this work was the first to show
that merging classical programming techniques with synthesis
techniques is beneficial and can be done successfully.
This is joint work with
Roderick Bloem,
Andreas Griesmayer, and
Stefan Staber.
 Synthesis from Specification in LinearTime Temporal Logic
(LTL). In this line of work, we aim to construct the complete control
logic of a system from desired safety and liveness properties. We
developed the first tools that are able to automatically construct
circuits from temporal specifications. Our tool
Anzu
(CAV08) is able to
construct correct circuits from industrial specifications
(DATE07,
COCV07,
JCSS11),
including an arbiter for ARM's advanced highperformance bus. I
furthermore designed and implemented
Lily, the first tool to
automatically synthesize finitestate systems from a specification
given by an arbitrary LTL formula
(FMCAD06).
This is joint work with
Roderick Bloem,
Stefan Galler,
Nir Piterman,
Amir Pnueli,
Yaniv Sa'ar, and
Martin Weiglhofer.

Quantitative Verification and Synthesis. Inspired by my work on
automatically constructing systems, we observed that classical
specifications are in many cases not expressive enough for
synthesis. The reason is that many design decisions are tradeoffs
between different degrees of freedom, all subject to constraints. For
example, one might aim for a system that is sufficiently fast but
consumes little energy, which conflicts with the desired
performance. We were the first to develop the theory and tools that
allow the designer to use quantitative specifications to state soft
constraints to guide the synthesis process. Such quantitative
specifications map a system behavior to a real value instead of a
Boolean value, indicating how good this particular behavior is. Given
a set of hard constraints and a set of soft constraints, our approach
automatically derives implementations that satisfy the hard
constraints and optimize the soft constraints with respect to the
worstcase environment
(CAV09)
or with respect to an averagecase
environment
(CAV10,
TACAS11). Furthermore, our framework allows us to
construct robust systems, which behave reasonably even in case of
unanticipated behavior of the environment
(FMCAD09,
CAV10). Most
recently, I have developed with my students a specification framework
and an underlying semisymbolic algorithm to automatically construct
efficient systems
(VMCAI12). We define efficiency as the ratio between
given costs and rewards. This meets our initial goal of capturing the
tradeoffs arising in a design process. Our most recent implementation
can generate (in a matter of seconds) efficient controllers for
systems with several millions of states.
This is joint work with
Roderick Bloem,
Krishnendu Chatterjee,
Karin Greimel,
Thomas A. Henzinger,
Rohit Singh, and
Christian von Essen.

ComponentBased Design and Synthesis. Because many large
systems are constructed in a component based manner, I also have
worked on (i) models for componentbased systems and (ii) the
automatic construction of prioritybased controllers for
componentbased systems. More precisely, we extended a theory to
describe interfaces between components with a shared refinement
operator
(EMSOFT08). Our new operator allows us to model component reuse,
which was not possible in previous theories. Furthermore, we developed
a theory and a tool to synthesize priorities between actions in a
componentbased model to ensure safety properties or avoid deadlocks
in the system
(ATVA11,
NFM11,
CIAA11).
This is joint work with
Saddek Bensalem,
ChihHong Cheng and
his collaborators at fortiss,
Laurent Doyen,
Thomas A. Henzinger,
Tatjana Petrov, and
Rongjie Yan.
 Quality of Specifications. The synthesized system is only
as good as the specification from which it is derived. I have worked
on approaches to improve the quality of specifications. We developed
and implemented an approach that, given a specification for a system,
constructs necessary assumptions on the environment of the system,
automatically turning formally useless specifications into useful ones
(CONCUR08,
CAV10). We also introduced a new notion of equivalence between
specifications of systems, provided lower and upper bounds, and
presented an optimal algorithm for the corresponding decision problems
(ICALP08). Our notion is coarser than the traditional one; it considers
formulas equivalent that are distinguishable in other
formalisms. Therefore, a synthesis or verification task can be
performed with simpler formulas, leading to more efficient
implementations.
This is joint work with
Roderick Bloem,
Krishnendu Chatterjee,
Karin Greimel,
Thomas A. Henzinger,
Arjun Radhakrishna, and
Moshe Vardi
 Additional Research Directions. I have also worked on and
continue to have interest in synthesis techniques for unbounded data
domains
(FMCAD10, joint work with
Jad Hamza and
Viktor Kuncak),
as well as the analysis of population models in
systems biology (
Reachability Problems 2009,
Journal of Foundations of Computer Science 2011), joint work with
Thomas A. Henzinger and
Verena Wolf)
software transactional memory algorithms
(PLDI08,
joint work with
Rachid Guerraoui,
Thomas A. Henzinger, and
Vasu Singh),
and business process models
(BPM08, joint work
with
Dirk Fahland,
Cedric Favre,
Jana Koehler,
Niels Lohmann,
Hagen Völzer, and
Karsten Wolf).
My research in a word cloud.
