Verimag Verimag CNRS
[Home] [News] [Research] [Students] [Committees] [Teaching] [Publications] [Projects]

Synthesis-Augmented 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 deadlock-free is easy, yet developing a system that is deadlock-free 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 trade-offs 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 C-like code (e.g., a Traffic Collision Avoidance System and a simple DLX-style processor, see JCSS12 for details). Together with program sketching (Solar-Lezama 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 Linear-Time 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 high-performance bus. I furthermore designed and implemented Lily, the first tool to automatically synthesize finite-state 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 trade-offs 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 worst-case environment (CAV09) or with respect to an average-case 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 semi-symbolic 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 trade-offs 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.

  • Component-Based Design and Synthesis. Because many large systems are constructed in a component- based manner, I also have worked on (i) models for component-based systems and (ii) the automatic construction of priority-based controllers for component-based 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 component-based model to ensure safety properties or avoid deadlocks in the system (ATVA11, NFM11, CIAA11).
    This is joint work with Saddek Bensalem, Chih-Hong 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.