BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of Imperative Programs Through Characteristic Formula
 e - Arthur Charguéraud\, INRIA
DTSTART:20101118T130000Z
DTEND:20101118T140000Z
UID:TALK27882@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In my thesis\, I have developed a new approach to program veri
 fication\, based on characteristic formulae. The characteristic formula of
  a program is a higher-order logic formula that describes the behaviour of
  that program\, in the sense that it is sound and complete with respect to
  the semantics. This formula can be exploited in an interactive theorem pr
 over to establish that a program satisfies a specification expressed in th
 e style of Separation Logic. One key feature of characteristic formulae is
  that they are of linear size and that they can be pretty-printed just lik
 e the source code they describe.\n\nCharacteristic formulae serve as a bas
 is for a tool\, called CFML\, that supports the verification of Caml progr
 ams using the Coq proof assistant. I have used this tool to verify about h
 alf of the content of Okasaki's book on purely functional data structures.
  I have also verified a collection of small but tricky imperative function
 s\, such as higher-order iterators on mutable lists\, the in-place list re
 versal function\, the CPS-append function\, as well as fixed point combina
 tors.\nIn the talk\, I will explain how to construct characteristic formul
 ae and show how CFML works in practice.\n
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR