On Thursday 2015-06-11, at 10h30, in room Byron Blanc,
Speaker: Isabela Drãmnesc
Title: Proof-based Synthesis of Algorithms on Binary Trees
Abstract:
Program synthesis is currently a very active area of programming language and verification communities. We address the problem of synthesizing sorting algorithms operating on binary trees.
We develop several proof techniques by extending our previous work on the synthesis of algorithms on lists. We design appropriate induction principles and various prove-solve methods mixing rewriting with assumption-based forward reasoning and goal-based backward reasoning.
The proof techniques are implemented in the Theorema system and are used for the automatic synthesis of several sorting algorithms and for some auxiliary functions. For some of the synthesized algorithms we check the correctness in the Coq system.
