Nov 20 (Fri) RM#212

14:10-14:15 opening
14:15-15:15 session 1

矢田部 俊介 Shunsuke YATABE
"Specification check tool S3 and its mathematical model"

木下 佳樹 Yoshiki KINOSHITA
"Landau in Agda"

15:30-17:00 session 2

藤原 拓也 Takuya FUJIWARA
(Formalization and Safety Verification of Garbage Collection Algorithms with the Isabelle/HOL Proog Assistent)

吉丸 始須雄 Shizuo YOSHIMARU
(Methodology for Proving Properties over the Data with Different Induction Schemes)

番原睦則 Mutsunori BANBARA
(Sugar: A SAT-based Constraint Solver)

18:30- party
トラットリア ピアット(Trattoria Piatto)
Nov 21 (Sat) RM#211
9:30-10:30 session 3

武山 誠 Makoto TAKEYAMA
"Assurance cases in Agda : Incorporating informality"

(Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS)

10:45-11:45 session 4

"A certified interpreter for a subset of OCaml"

二木 厚吉 Kokichi FUTATSUGI
"Combining Inference and Search in Verification with CafeOBJ"

12:45-14:15 session 5 [TPPmark2009]

(Solutions of a common problem on undirected graphs and spanning trees)

Solutions by Daniel GAINA(CafeOBJ), Yasuhiko Minamide(Isabelle/HOL), and others.

*** Please present solutions by your favorite proof assistant. ***

14:15-14:20 closing