日米科学協力事業「ソフトウェア検証の論理的方法」更新のための企画研究

2003 年度 実績報告書

• 研究課題/領域番号: 15630002
• 研究機関: 慶應義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• 研究分担者: 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971) ; 萩谷 昌己 東京大学, 大学院・理学研究科, 教授 (30156252) ; 佐藤 雅彦 京都大学, 工学部, 教授 (20027387) ; 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286) ; 小林 直樹 東京工業大学, 工学部, 助教授 (00262155)
• キーワード: 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論

研究概要

これまでの日米共同研究の成果を基にして平成15年度にこの日米共同研究プロジェクトを発展的に継続すべく研究計画の企画を日米間で行った。米国側は本年より同様な企画のため、若い世代に中核メンバーを移行しながら日米共同研究の更新の準備を開始しており、日本側も本企画研究の遂行過程で若手世代に移行していく計画を進めた。現在までは日本側は岡田(慶応大)が、又米国側はScedrov(ペンシルバニア大)、Mitchell(スタンフォード大)が幹事役として共同研究や共同主催国際会議の企画を行い、これら幹事役と同世代の研究者達が井同研究の中核となってきた。(過去3年間に3回の日米ワークショップ及び特定領域「安全」グループ(代表:米澤教授(東大))と連携したソフトウェア安全性に関する国際シンポジウムを開催し、Theoretical Computer Science誌特別号、States-of-Art Series of LNCS (Springer)等を編集し、日米共同研究の成果発表も行ってきた。)今回の企画研究ではこれらの成果やこれまでの共同研究体制を分析し、今後の改良点を検討した。米国側からScedrov、Cervesato、Nuclaらが秋に来日し今後の共同研究の企画立案を行った。特にソフトウェア及びネットワークコミュニケーションの安全性検証のための共同研究の方法論を検討した。我々のソフトウェア検証の論理的方法についての日米共同研究は欧州やカナダ等の研究グループの研究とも深く関連するため、これらの研究グループとも打合せをして我々の研究企画に役立てた。

研究成果

• [文献書誌] H.Kushida, M.Okada: "A proof-theoretic study of the correspondence of classical logic and model logic"Journal of Symbolic Logic. 68・4. 1403-1414 (2003)
• [文献書誌] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)
• [文献書誌] H.Hasebe, J-P.Jouannaud, A.Kremer, M.Okada, R.Zumkeller: "Formal Verification of Dynamic Real-Time State-Transition Systems Using Linear Logic"日本ソフトウェア科学会第20回全国大会予稿集. (2003)
• [文献書誌] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)
• [文献書誌] M.Konovitch, Mitsuhiro Okada, A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. 294. 525-549 (2003)
• [文献書誌] M.Nagayama, Mitsuhiro Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. 294. 551-573 (2003)
• [文献書誌] M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security, Proceedings of the International Symposium on Software Security, 2002"Springer, Hot-topic Series. (2003)