Automated Revision of Distributed and Real-Time Programs

Опубликовано 6 сентября 2016, 17:00

The theory of automated program revision studies possibilities and limitations of revising existing programs. We require that such revision must be achieved within the given program's current state space so that the revised program satisfies newly identified requirements while it continues to satisfy its current properties. The main focus of this theory is to identify instances where automated revision of programs can be achieved efficiently (possibly in polynomial-time) and where it is difficult (i.e., hard in some class of complexity). Thus far, the theory has been established in two contexts: (1) adding properties to existing programs in closed systems where programs do not interact with the environment, and (2) adding properties to programs in open systems where programs are subject to a set of faults imposed by the environment. In this talk, I will present our results on automated synthesis of fault-tolerant distributed programs. Our synthesis algorithms have been implemented in the tool SYCRAFT which is capable of synthesizing fault-tolerant distributed programs with state space of size 10^30 and beyond.