皆様、

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

小林直樹 東京大学大学院情報理工学系研究科コンピュータ科学専攻 〒113-0033 東京都文京区本郷7-3-1 Phone: 03-5841-4124 Fax: 03-5841-4124 email: [email protected]

================== 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.