Concurrent Software Synthesis: Old Challenge - New Ideas

VCLA will be hosting a RiSE seminar talk by Doron Peled on May 23rd, 2013.

ABSTRACT

Automatic construction (synthesis) of correct-by-design software, directly from specification is, of course, more desirable than 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 was shown, under some simple assumptions, to be undecidable.

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.