University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Verification of Imperative Programs Through Characteristic Formulae

Verification of Imperative Programs Through Characteristic Formulae

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity