Campus Event Calendar
Event Entry
What and Who
Formal Program Verification Through Characteristic Formulae
Arthur Chargueraud
INRIA
SWS Colloquium
SWS, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 25 March 2010
11:00
90 Minutes
E1 5
5th floor
Saarbrücken
Abstract
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.
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.
Contact
Claudia Richter
9325 688
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Claudia Richter, 03/17/2010 10:53 -- Created document.