CAREER: Tractable Formal Methods for the Synthesis of Concurrent Programs

9702616 The problem of developing concurrent programs from formal specifications is addressed. Concurrent programs consist of a set of interacting components each running on a single computer. A formal specification states precisely the correct behavior required of the program. The project investigates automatic program synthesis: given a formal specification, the synthesis method automatically produces a correct program. Synthesis obviates the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of previous synthesis methods is that they are too inefficient to generate any but the smallest programs. The objective is to produce synthesis methods sufficiently efficient to synthesize large concurrent programs. The approach taken uses "pairwise analysis." Previous approaches considered all program components simultaneously, requiring the analysis of a very large number of combined behaviors. This research looks only at pairs of components at any one time, greatly reducing the analytical burden. Almost all large, practical programs are concurrent; the interaction among their many independent components is very difficult to design properly. The significance and impact of this research is that it will eventually provide conceptual tools to help programmers create such programs and analyze whether their behavior conforms to the program specification. ***