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. ***

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Communication Foundations (CCF)
Application #
9702616
Program Officer
Frank D. Anger
Project Start
Project End
Budget Start
1997-05-01
Budget End
2000-09-30
Support Year
Fiscal Year
1997
Total Cost
$148,673
Indirect Cost
Name
Florida International University
Department
Type
DUNS #
City
Miami
State
FL
Country
United States
Zip Code
33199