BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Semi-automatic Algorithm Synthesis (Case Study: Square Root) - Mad
 alina Erascu - Research Institute for Symbolic Computation\, Johannes Kepl
 er University\, Linz\, Austria
DTSTART:20120621T120000Z
DTEND:20120621T130000Z
UID:TALK38374@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:We report a case study on semi-automatic synthesis of optimal 
 algorithms for square root problem: given the real number x and the error 
 bound e\, find the real interval such that it contains the radical of x an
 d its width is less than e. As usual\, we begin by fixing an algorithm sch
 ema\, namely\, iterative refining: the algorithm starts with an initial in
 terval and repeatedly updates it by applying a refinement function\, say f
 \, on it until it becomes narrow enough. Then the synthesis amounts to fin
 ding a refinement function f that ensures that the algorithm is correct (l
 oop invariant)\, terminating (contraction)\, and optimal. All these can be
  formulated as quantifier elimination over the real numbers. Hence\, in pr
 inciple\, they can be all carried out automatically. However the computati
 onal requirement is so huge\, making the automatic synthesis practically i
 mpossible with the current general quantifier elimination software. Hence\
 , we did some hand derivations and were able to synthesize semi-automatica
 lly an optimal algorithm under suitable assumptions. We hope that the idea
 s behind the hand derivations could be eventually turned into an algorithm
 . Then we would have an automatic synthesis of optimal square-root algorit
 hm. This is joint work with Hoon Hong.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR