形式的に検証可能なプログラム変換フレ.ムワ.クの構築

• 研究課題/領域番号: 20500011
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 京都大学
• 研究代表者: 西村 進 京都大学, 大学院・理学研究科, 准教授 (10283681)
• 研究期間 (年度): 2008 – 2011
• 研究課題ステータス: 完了 (2011年度)
• 配分額: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円); 2011年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2010年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2009年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2008年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
• キーワード: プログラム理論 / プログラム変換 / 形式的証明 / 形式的検証 / 並行プログラム

研究概要

ポインタ操作や例外処理のような進んだ計算機構を含むプログラムに対してプログラムの段階的詳細化の手法を拡張することによって、プログラムの正しさを保証しながらプログラム変換を行う手法を与えた。論理体系としては、ポインタ操作にはseparation logic,例外処理には4値論理がそれぞれ対応することを示し、計算機上でそれぞれの論理体系に基づく形式的証明を行うことによってプログラム変換の正当性を保証することができることを示した。

研究成果

• [雑誌論文] Refining Exception s in Four-Valued Logic (2010)
  • 著者名/発表者名: Susumu Nishimura
  • 雑誌名: 19th Internatio nal Symposium, LOPSTR 2009, Revised Selected Papers ページ: 113-127
  • URL: http://dx.doi.org/10.1007/978-3-642-12592-8_9
• [雑誌論文] Refining Exceptions in Four-Valued Logic (2010)
  • 著者名/発表者名: Susumu Nishimura
  • 雑誌名: 19th International Symposium, LOPSTR 2009, Revised Selected Papers (Lecture Notes in Computer Science) vol.6037 ページ: 113-127
  • 査読あり
• [雑誌論文] Refining Exceptions in Four-Valued Logic (2010)
  • 著者名/発表者名: Susumu Nishimura
  • 雑誌名: 19th International Symposium, LOPSTR 2009, Revised Selected Papers (Lecture Notes in Computer Science) 6037(掲載決定)
  • 査読あり
• [雑誌論文] Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement (2008)
  • 著者名/発表者名: Shin-ya Katsumata, Susumu Nishimura
  • 雑誌名: Journal of Functional Programming 巻: vol.18(5-6) ページ: 781-819
  • URL: http://dx.doi.org/10.1017/S095679680800693X
• [雑誌論文] Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement (2008)
  • 著者名/発表者名: Shin-ya Katsumata, Susumu Nishimura
  • 雑誌名: Journal of Functional Programming vol.18(5-6) ページ: 781-819
  • 査読あり
• [雑誌論文] Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement (2008)
  • 著者名/発表者名: Shin-ya Katsumata, Susumu Nishimura
  • 雑誌名: Journal of Functional Programming 18(5-6) ページ: 781-819
  • 査読あり
• [雑誌論文] May&Must-Equivalence of Shared Variable Parallel Programs in Game Semantics
  • 著者名/発表者名: Keisuke Watanabe, Susumu Nishimura
  • 雑誌名: 情報処理学会論文誌プログラミング 巻: (掲載確定)
  • NAID: 130003324428
  • 査読あり
• [学会発表] May&Must-Equivalence of Shared Variable Parallel Programs in Game Semantics (2012)
  • 著者名/発表者名: Keisuke Watanabe, Susumu Nishimura
  • 学会等名: 情報処理学会プログラミング研究会
  • 発表場所: 産業総合研究所つくば中央
  • 年月日: 2012-03-16
• [学会発表] Calculating Tree Navigation with Symmetric Relational Zipper (2011)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップPPL2011
  • 発表場所: 札幌
  • 年月日: 2011-03-10
• [学会発表] Calculating Tree Navigation with Symmetric Relational Zipper (2011)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: The 20th ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM' 11)
  • 発表場所: Austin, Texas, アメリカ合衆国
  • 年月日: 2011-01-25
• [学会発表] Calculating Tree Navigation with Symmetric Relational Zipper (2011)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: The 20th ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM'11)
  • 発表場所: Austin, Texas,アメリカ合衆国
  • 年月日: 2011-01-25
• [学会発表] May & Must-Equivalence of Shared Variable Parallel Programs in Game Semantics (2011)
  • 著者名/発表者名: Keisuke Watanabe, Susumu Nishimura
  • 学会等名: 情報処理学会プログラミング研究会
• [学会発表] Calculating Tree Navigation with Symmetric Relational Zipper (2011)
  • 著者名/発表者名: Yuta Ikdeda, Susumu Nishimura
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップ
• [学会発表] Calculating Tree Navigation with Symmetric Relational Zipper (2011)
  • 著者名/発表者名: Yuta Ikdeda, Susumu Nishimura
  • 学会等名: The 20th ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation
  • URL: http://dx.doi.org/10.1145/1929501.1929521
• [学会発表] Refining Exceptions in Four-Valued Logic (2009)
  • 著者名/発表者名: 西村進
  • 学会等名: 代数,論理,幾何と情報科学研究集会(ALGI20)
  • 発表場所: 鳥取環境大学
  • 年月日: 2009-09-15
• [学会発表] Refining Exceptions in Four-Valued Logic (2009)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 19^<th> International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR 2009
  • 発表場所: Coimbra, ポルトガル
  • 年月日: 2009-09-10
• [学会発表] Refining Exceptions in Four-Valued Logic (2009)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 代数,論理,幾何と情報科学研究集会
• [学会発表] Refining Exceptions in Four-Valued Logic (2009)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 19th International Symposium
• [学会発表] Safe Modification of Pointer Programs in Refinement Calculus (2009)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 9th International Conference on Mathematics of Program Construction
  • URL: http://dx.doi.org/10.1007/978-3-540-70594-9_16
• [学会発表] Safe Modification of Pointer Programs in Refinement Calculus (2008)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: Internatlonal Conference on Mathematics of Program Construction (MPC'08)
  • 発表場所: CIRM, Marseille, フランス
  • 年月日: 2008-07-15
• [学会発表] Safe Modification of Pointer Programs in Refinement Calculus (2008)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: International Conference on Mathematics of Program Construction (MPC'08)
  • 発表場所: CIRM, Marseille, France
  • 年月日: 2008-07-15
• [備考] ホームページ等MPC 2008発表論文に関する、形式的証明のダウンロード
  • URL: http://www.math.kyoto-u.ac.jp/~susumu/mpc08pvs/index.html
• [備考]
  • URL: http://www.math.kyoto-u.ac.jp/~susumu/mpc08pvs/index.html
• [備考]
  • URL: http://www.math.kyoto-u.ac.jp/~susumu/mpc08pvs/index.html