Concurrent Software Synthesis: Old Challenge – New Ideas

Date: 16:00, Thursday, May 23, 2013
Speaker: Doron Peled
Venue: TU Wien

Automatic construction (synthesis) of correct-by-design software,
directly from specification is, of course, more desireable thant the
usual software development process. The latter typically includes
several cycles of coding, testing or automatic verification at
different development levels, and new errors may be introduced even
when attempting to remove the old ones. While automatic verification
is already provably and and practically difficult, code synthesis has
an ever higher, prohibitive, complexity. Even worse, the automatic
construction of concurrent code iwas shown, under some simple
assumptions, to be undecideable.

In this lecture, I will present some recent results and ideas that try
to circumvent the classical dead-end results on concurrent software
synthesis.
The first techniques uses a combination of model checking and genetic
programming in a, mostly automatic, process of finding correct code
from
temporal specification. The second technique will add control to an
existing concurrent system in order to impose further properties to an
existing code. This is done using logic of knowledge, and with the
relaxing assumption that additional interactions between processes may
be added, when needed.
The third technique will be based on using a high level, large granularity,
modeling formalism, which can be used for the high level design of the
system and can be implemented simply and automatically on standard
concurrent architectures.

The lecture would assume only very basic familiarity of logic and concurrent
modeling of systems.

Posted in RiSE Seminar