Theorem Proving and Provers Meeting (1st TPP), 28-29th November 2005, JAIST
November 28th, 13:30-15:45 Verifying concurrent processes
Place: Collaboration Room 7 (IS school, 5F)
-
磯部祥尚（AIST）
CSP-Prover: a Theorem Prover for a Process Algebra CSP
--- Towards the Verification of Concurrent Processes ---
-
河辺義信 (NTT) IOA-Toolkit and Larch Prover
-
高木理 (京都産業大) On objects of deductive verifications
November 28th, 16:00-17:30 Cafe/OBJ
November 28th 19:00- Party
いたる本店
approx. 6000yen/person (will set student discount)
November 29th 10:15-12:30 Formal Reasoning
November 29th 13:30-15:45 Twelf/Isabelle session
-
亀山幸義、吉原宏之（筑波大）
Metatheorem Proving in Twelf and Its Semantics
-
南出靖彦（筑波大）
A Case Study in Verification of C Programs: the Tortoise Hare Algorithm
-
櫻田英樹 (NTT) Protocol Verification on Isabelle/HOL
November 29th 16:00-17:15 Last session