Open seminar: Deductive and Inductive Methods for Program Synthesis

Date: May 04, 2004 (Tuesday) at 15:30

Speaker: Jaan Penjam (Tallinn, Estland)
Joint seminar organized by Mathematical Colloquium, Center of Mathematical Sciences and Department of Computer Science
Formal specifications that define required system properties play a central role in software engineering. They can be used for reasoning about complex programs on a suitable abstract level. Formal models are inescapable when programs are automatically derived or verified. The most widely used techniques for automatic program construction are based on stepwise refinement of a specification until a program code is achieved.

In this seminar talk, I will consider different approaches for program generation where programs are obtained by means of special mathematically based manipulations, without construction of intermediate level specifications. In particular, I will briefly introduce a method based on proof search, known as structural synthesis of programs (SSP), and on the other hand, a technique based on the optimization of a specific fitness function related to the task to be solved. SSP has been implemented in a couple of commercial and some experimental systems that are basically of scientific or pedagogical value. SSP's most advanced implementation is in the system NUT performed jointly by the researchers of the Institute of Cybernetics (Tallinn) and Deparment of Teleinformatics of KTH.

The SSP method is a deductive approach for program synthesis carried out via special logical inference rules from a general relational specification of a problem. This specification is often called the computational model of the problem. Here we are going to design an inductive approach for automatic program construction based on the same specification language (computational model) that is augmented by experimental data that describedesirable input-output behavior of the program to be composed. A common specification would bridge deductive and inductive methods of program construction. We believe that combining these two types of techniques might provide more general and effective procedures for automation of software development. This would simulate human reasoning where deductive inference steps are interleaved with drawing conclusions from samples of experimental data. In my talk I will introduce the idea of inductive program construction as well as an algorithm for coding sequential programs by real numbers that allow transforming a task for program synthesis into an optimisation problem that could be solved using evolutionary programming techniques.

Room: MH:C

Last modified Dec 9, 2011 12:59 pm