[logic-ml] Talk by Quentin Heath, 29 Sept.

[koba at kb.is.s.u-tokyo.ac.jp]

皆様、

東京大学の小林です。
以下のとおり講演会を開催いたしますので、ご興味のある方はお集まりください。

小林直樹
東京大学大学院情報理工学系研究科コンピュータ科学専攻
〒113-0033 東京都文京区本郷7-3-1
Phone: 03-5841-4124
Fax: 03-5841-4124
email: koba at is.s.u-tokyo.ac.jp


==================
Time: 3:00pm, Thursday, the 29th September
Place: Room 214, 7th Building of Faculty of Science
     （理学部7号館）

Title: Proof certificates as proof theory for model checking

Speaker:
Quentin Heath (LIX, Ecole polytechnique)

Abstract: 

 Model checking has proved valuable on its own for locating errors in
 finite state computer models and specifications.  However, model
 checkers can also be used to prove properties that will be consumed by
 other computational logic systems, such as theorem provers.  In order
 for the model checker to be trusted by an external tool, we ask that it
 outputs its ``proof evidence'' as a formally defined document---a proof
 certificate---and that this document is checked by a trusted proof
 checker.

 We propose such a proof checker based on a first-order variant of linear
 logic, and justify why this logic is appealing as a foundation for model
 checking.  We also provide a proof system for this logic, and tie in the
 notion of proof certificates in a way that makes proof checking sound
 for a minimal amount of work.

 As a result, a range of model checking computations can be imported in
 formal proofs and certified by a proof checker that is simple, non
 idiosyncratic, and easy to certify.