"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.
|Zeit:||Donnerstag, 25.03.2010, 11.00 Uhr|
|Ort:||Saarbrücken, Wartburg, Raum 410|
|Hinweis:||Der Vortrag wird live nach Kaiserslautern Gebäude 49, Raum 206 übertragen.|