BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On Synthesis of Verification Tools - Andrey Rybalchenko\, Technisc
 he Universität München
DTSTART:20120925T090000Z
DTEND:20120925T100000Z
UID:TALK39131@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Software complexity is growing\, so is the demand for software
  verification. Soon\, perhaps within a decade\, wide deployment of softwar
 e verification tools will be indispensable or even mandatory to ensure sof
 tware reliability in a large number of application domains\, including but
  not restricted to safety and security critical systems. To adequately res
 pond to the demand we need to eliminate tedious aspects of software verifi
 er development\, while providing support for the accomplishment of creativ
 e aspects. We believe that the next generation of software verifiers will 
 be constructed from logical specifications designed by quality/verificatio
 n engineers with expertise in the application domain. Give a specification
  describing a verification method\, a corresponding software verifier will
  be obtained by implementing a frontend that translates software source co
 de into constraints according to the specification and then coupling the f
 rontend with a highly-tuned general-purpose constraint solver\, thus elimi
 nating the need for algorithmic implementation efforts from the ground up.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR