BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification and Synthesis by Sciduction -  Sanjit Seshia\, Univer
 sity of California\, Berkeley
DTSTART:20120419T143000Z
DTEND:20120419T153000Z
UID:TALK37543@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Even with impressive advances in automated formal methods\, ce
 rtain problems in system verification and synthesis remain challenging.\n\
 nExamples include the verification of quantitative properties of software 
 involving constraints on timing and energy consumption\, and the automatic
  synthesis of systems from specifications. The challenges mainly arise fro
 m three sources: environment modeling\, incompleteness in specifications\,
  and the complexity of underlying decision problems.\n\nIn this talk\, I w
 ill present SCIDUCTION\, a methodology to tackle these challenges. Sciduct
 ion combines inductive inference (learning from examples)\, deductive reas
 oning (such as SAT/SMT solving)\, and structure hypotheses.\n\nWe have dem
 onstrated several applications of sciduction including timing analysis of 
 embedded software\, synthesis of loop-free programs\, synthesis from tempo
 ral logic (LTL)\, term-level verification of hardware (RTL) designs\, and 
 switching logic synthesis of hybrid systems. This talk will present some c
 ore theory\, a couple of illustrative applications\, and directions for fu
 ture work.
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR