Personal tools
You are here: Home / Internal / RISC Forum / 2016 / RISC Forum

RISC Forum

David Cerna: Conference SCSS16; Xinhua Xiong: Self-introduction; Tudor Jebelean: Proof-based Synthesis of Sorting Algorithms for Trees
When Apr 11, 2016
from 01:30 PM to 02:30 PM
Where Seminar room castle
Add event to calendar vCal
iCal

We develop various proof techniques for the synthesis of sorting algorithms on binary trees, by extending our previous work on the synthesis of algorithms on lists. Appropriate induction principles are designed and various specific prove-solve methods are experimented, mixing rewriting with assumption-based forward reasoning and goal-based backward reasoning a la Prolog. The proof techniques are implemented in the Theorema system and are used for the automatic synthesis of several algorithms for sorting and for the auxiliary functions, from which we present few here. Moreover we formalize and check some of the algorithms and some of the
properties in the Coq system.

« April 2025 »
April
MoTuWeThFrSaSu
123456
78910111213
14151617181920
21222324252627
282930
Upcoming Events
RISC Forum Apr 07, 2025 01:30 PM - 01:45 PM
NO RISC Forum (lecture free) Apr 14, 2025 01:30 PM - 01:45 PM
NO RISC Forum Apr 21, 2025 01:30 PM - 01:45 PM
RISC Forum Apr 28, 2025 01:30 PM - 01:45 PM
FIRST AID COURSE May 05, 2025 01:00 PM - 05:00 PM
Previous events…
Upcoming events…