• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

Using Parallel Computations in Deductive Synthesis of Functional Programs

P. 67-72.
Korukhova Y., Fastovets N.
The paper deals with deductive synthesis of functional programs. This approach means that we take as our input data a specification of program, it is treated as a mathematical existence theorem and while proving it constructively we derive a program. If the derivation is successful the resulted program does not require verification: it is proven that it corresponds to all the specified requirements. Despite the fact that there are several theoretical methods that gives the rules for proof construction and program derivation they usually do not work in automated synthesis systems because of exponentially growing search space of possible proof attempts. We are trying to solve this problem using recent changes in computer architecture: the possibility of parallel execution of proofs or their steps is discussed. The proposed ideas were implemented in the system Icarus and used for the synthesis of some examples.   

In book

Edited by: M. O'hEigeartaigh, N. Popova. Waterford: Waterford Institute of Technology, 2014.