Logic-based program synthesis: state-of-the-art and future trends

Constructing certifiably reliable software systems is difficult. Deductive program synthesis techniques (Flener 1995, Manna and Waldinger 1980) 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. Amphion and Meta-Amphion Amphion (Stickel, et al. 1994) is a deductive synthesis system that has been used to construct programs in the domains of celestial mechanics and avionics. The experiences gained in the Amphion system mirror experiences in other synthesis systems. Amphion is a domain-independent system that is tailored to a domain in part through the creation of a declarative domain theory. Problem specifications are solved by programs constructed of sequences of calls to software components. Program construction is entirely automated. Programs have been generated that are currently in use by space scientists planning observations for the Cassini mission to Satur