BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Software Synthesis using Automated Reasoning - Ruzika Piskac\, EPF
 L
DTSTART:20110328T090000Z
DTEND:20110328T100000Z
UID:TALK30413@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Software synthesis is a technique for automatically generating
  code from a given specification. The goal of software synthesis is to mak
 e software development easier while increasing both the productivity of th
 e programmer and the correctness of the produced code. In this talk I will
  present an approach to synthesis that relies on the use of automated reas
 oning and decision procedures. First I will describe how to generalize dec
 ision procedures into predictable and complete synthesis procedures. Here 
 completeness means that the procedure is guaranteed to find code that sati
 sfies the given specification. I will illustrate the process of turning a 
 decision procedure into a synthesis procedure using linear integer arithme
 tic as an example. Next I will outline a synthesis procedure for specifica
 tions given in the form of type constraints. The procedure takes into acco
 unt polymorphic type constraints as well as code behavior. The procedure d
 erives code snippets that use given library functions. I will conclude wit
 h an outlook on possible future research directions in synthesis and decis
 ion procedures for software reliability. I believe that these techniques c
 an make programming easier and more reliable by combining program analysis
 \, software synthesis\, and automated reasoning.\n
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR