[12-2]Synthesis of Designs from Property Specifications

Date:2008-11-24

Title: Synthesis of Designs from Property Specifications
Speaker: Prof. Amir Pnueli,  New York University and Weizmann Institute (Emeritus)
Time: 10am, Tuesday Dec. 2
Venue: Lecture room, Lab for Computer Science, Level 3 Building #5

About the speaker:

Prof. Amir Pnueli received the Turing Award in 1996 for seminal work introducing temporal logic into computing science and for outstanding contributions to program and systems verification.

Abstract:

The current state of the art uses specification of properties in a behavioral form, such as linear temporal logic, mainly for static and dynamic verification of implementations of reactive systems, AFTER they have been constructed. In the talk we consider the more radical approach by which a specification in terms of its desired properties is formed at the beginning of a system development, before any implementation is attempted. After some analysis and validation of this specification, one may apply a synthesis algorithm in order to automatically derive a correct-by-construction implementation. No further verification or testing is required.

While this has been considered an unachievable dream for a long time, recent progress in the algorithms for synthesis has made design synthesis from property specification applicable for medium size designs.

In the talk, we provide more details about the problem of synthesizing digital designs from their LTL (and similar) specifications. In spite of the theoretical double exponential lower bound, we show that for many expressive specifications of hardware designs the problem can be solved in time N^3. We describe the context of the problem, as part of the Prosyd European Project which aims to provide a property-based development flow for hardware designs. Within this project, synthesis plays an important role, first in order to check whether a given specification is realizable, and then for synthesizing part of the developed system.