" Synthesis-Augmented System Development"

Abstract:

Synthesis translates a high-level system description into an executable implementation. In this talk, I give an overview of my work on synthesizing reactive systems, which led to the first tools that automatically construct, from temporal specifications, digital circuits, such as an arbiter for ARM's advanced high-performance bus. Then, I present two approaches that augment the current system design process with synthesis-based techniques.

Our first approach automatically localizes and repairs faults in the control structure of a program that violates a given temporal specification. It is based on solving automata-based games on infinite sequences. We applied it to Verilog and C-like code, such as a Traffic Collision Avoidance System and a simple DLX-style microprocessor design.

The second approach enables the designer to explore the trade-off between conflicting objectives, e.g., the speed of a car versus its fuel consumption, or the transmission rate of a wireless device versus its energy consumption. Our approach automatically constructs discrete controllers with optimal efficiency for a given probabilistic environment. The approach is based on finding optimal strategies for Markov Decision Processes with a novel objective function. We have integrated our approach in the popular model checker PRISM and applied it to several examples, such as a zero-configuration networking protocol.

Short Bio:

Barbara Jobstmann is a tenured researcher in Verimag, a joint laboratory of the French National Center of Scientific Research (CNRS) and the Universities of Grenoble, France. Before that, she was a postdoctoral researcher with Thomas A. Henzinger at the Ecole Polytechnique Federale de Lausanne (EPFL), Switzerland. She received a Ph.D. degree in Computer Science from the University of Technology in Graz, Austria under the supervision of Roderick Bloem. Her research focuses on constructing correct and reliable computer systems using synthesis techniques. She was contributing to the EU project PROSYD, COMBEST, and help initiating the project EU project ASCENS. She was a program committee chair of the ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) in 2010 and 2011.

___________________________________________________________________________