Verification of Imperative Programs Through Characteristic Formulae

Add to your list(s) Download to your calendar using vCal

• Arthur Charguéraud, INRIA
• Thursday 18 November 2010, 13:00-14:00
• Small lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

In my thesis, I have developed a new approach to program verification, 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 prover to establish that a program satisfies a specification expressed in the 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 like the source code they describe.

Characteristic formulae serve as a basis for a tool, called CFML , that supports the verification of Caml programs using the Coq proof assistant. I have used this tool to verify about half of the content of Okasaki’s book on purely functional data structures. I have also verified a collection of small but tricky imperative functions, such as higher-order iterators on mutable lists, the in-place list reversal function, the CPS -append function, as well as fixed point combinators. In the talk, I will explain how to construct characteristic formulae and show how CFML works in practice.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.