Abstract:
Constructing certifiably reliable software systems is difficult. Deductive program synthesis techniques can currently be used to construct small software systems or to organize small sets of software components in a reliable manner. In order for synthesis techniques to be applicable to real-world problems outside the experimental laboratory, they must be inexpensive relative to manual techniques. The difficulty and expense in constructing software synthesis systems currently precludes the use of these techniques in many instances.