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

2011 年度 研究成果報告書

• 研究課題/領域番号: 20500011
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 京都大学
• 研究代表者: 西村 進 京都大学, 大学院・理学研究科, 准教授 (10283681)
• 研究期間 (年度): 2008 – 2011
• キーワード: プログラム理論 / プログラム変換 / 形式的証明

研究概要

ポインタ操作や例外処理のような進んだ計算機構を含むプログラムに対してプログラムの段階的詳細化の手法を拡張することによって、プログラムの正しさを保証しながらプログラム変換を行う手法を与えた。論理体系としては、ポインタ操作には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
• [雑誌論文] 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
• [学会発表] May & Must-Equivalence of Shared Variable Parallel Programs in Game Semantics (2011)
  • 著者名/発表者名: Keisuke Watanabe, Susumu Nishimura
  • 学会等名: 情報処理学会プログラミング研究会
  • 年月日: 20110500
• [学会発表] Calculating Tree Navigation with Symmetric Relational Zipper (2011)
  • 著者名/発表者名: Yuta Ikdeda, Susumu Nishimura
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップ
  • 年月日: 20110000
• [学会発表] 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
  • 年月日: 20110000
• [学会発表] Refining Exceptions in Four-Valued Logic (2009)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 代数,論理,幾何と情報科学研究集会
  • 年月日: 20090000
• [学会発表] Refining Exceptions in Four-Valued Logic (2009)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: 19th International Symposium
  • 年月日: 20090000
• [学会発表] 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
  • 年月日: 20090000
• [備考] ホームページ等MPC 2008発表論文に関する、形式的証明のダウンロード
  • URL: http://www.math.kyoto-u.ac.jp/~susumu/mpc08pvs/index.html