Synthesis of Programs from Temporal Property Specifications
                               Amir Pnueli
       New York University and Weizmann Institute of Science (Emeritus)

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.

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.

The above results were obtained for the synthesis of synchronous
systems. In the talk, we will consider the generalization of the
problem to the case of asynchronous systems. This will enable the
synthesis of programs that communicate with their environments by
shared variables. We will mainly report about work in progress, which
provides different approaches and heuristics for establishing
unrealizability and realizability of asynchronous specifications.

This is a joint work with Nir Piterman, Yaniv Sa'ar, and Uri Klein.