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"
藤原 拓也 Takuya FUJIWARA
"証明支援系Isabelle/HOLによるごみ集めアルゴリズムの形式化と安全性検証"
(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
"SAT符号化に基づく制約ソルバーSugarの紹介"
(Sugar: A SAT-based Constraint Solver)
武山 誠 Makoto TAKEYAMA
"Assurance cases in Agda : Incorporating informality"
Reynald AFFELDT
"形式的な暗号学的安全性証明によるアセンブリプログラムの安全性検証：BBSの事例"
(Certifying Assembly with Formal Cryptographic Proofs: the Case of BBS)
Jacques GARRIGUE
"A certified interpreter for a subset of OCaml"
二木 厚吉 Kokichi FUTATSUGI
"Combining Inference and Search in Verification with CafeOBJ"
共通問題の解答とその比較：無向グラフと全域木
(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. ***