• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 15630002
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section企画調査
Research Field Fundamental theory of informatics
Research InstitutionKeio University

Principal Investigator

岡田 光弘  慶應義塾大学, 文学部, 教授 (30224025)

Co-Investigator(Kenkyū-buntansha) 二木 厚吉  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
萩谷 昌己  東京大学, 大学院・理学研究科, 教授 (30156252)
佐藤 雅彦  京都大学, 工学部, 教授 (20027387)
米崎 直樹  東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
小林 直樹  東京工業大学, 工学部, 助教授 (00262155)
Project Period (FY) 2003
Project Status Completed (Fiscal Year 2003)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2003: ¥2,100,000 (Direct Cost: ¥2,100,000)
Keywords論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論
Research Abstract

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

Report

(1 results)
  • 2003 Annual Research Report
  • Research Products

    (7 results)

All Other

All Publications (7 results)

  • [Publications] 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)

    • Related Report
      2003 Annual Research Report
  • [Publications] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] 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)

    • Related Report
      2003 Annual Research Report
  • [Publications] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] M.Konovitch, Mitsuhiro Okada, A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. 294. 525-549 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] M.Nagayama, Mitsuhiro Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. 294. 551-573 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 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)

    • Related Report
      2003 Annual Research Report

URL: 

Published: 2003-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi