Arthur Chargueraud

"Formal Program Verification Through Characteristic Formulae"

The characteristic formula of a program is a logical formula that implies any valid post-condition for that program. In this talk, I will explain how to build, in a systematic manner, the characteristic formula of a given purely functional Caml program, and then explain how one can use this formula to verify the program interactively, using the Coq proof assistant. This new, sound and complete approach to the verification of total correctness properties has been applied to the formalization of a number of data structures taken from Chris Okasaki's reference book. My presentation will include demos based on those case studies.

Bio: Arthur is finishing his PhD at INRIA-Rocquencourt under the supervision of François Pottier. His thesis work is on the verification of ML programs in Coq. He has also developed Coq-based tools for the mechanization of programming languages metatheory.
Arthur is applying for a post-doc position and will be hosted by Derek Dreyer.