ゲーム意味論に基づくリファインメント型の拡張とその応用

• 研究課題/領域番号: 25730035
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: ソフトウェア
• 研究機関: 筑波大学
• 研究代表者: 海野 広志 筑波大学, システム情報系, 助教 (80569575)
• 研究期間 (年度): 2013-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円); 2015年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2014年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2013年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
• キーワード: プログラム検証 / 型システム / 定理自動証明 / 制約解消 / リファインメント型 / 依存型 / ホーン節制約解消 / 制約最適化 / 関係的仕様 / 帰納的定理証明 / ゲーム意味論 / トレース意味論 / 抽象解釈 / 関係的仕様検証 / 停止性検証

研究成果の概要

本研究では、ソフトウェアの信頼性向上のために、高レベルプログラムの形式検証手法の一つであるリファインメント型システムおよびその型検査・推論法の、表示的意味論に基づく拡張を目指した。その主な成果として、代数データ構造を扱う高階関数型プログラムの(a)停止性、(b)非停止性、(c)関係的性質の全自動・高精度検証が可能な検証ツールRCamlの開発が挙げられる。

研究成果

• [雑誌論文] Temporal Verification of Higher-Order Functional Programs (2016)
  • 著者名/発表者名: Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
  • 雑誌名: In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices 巻: 51 (1) ページ: 57-68
  • DOI: 10.1145/2837614.2837667
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Refinement Type Inference via Horn Constraint Optimization (2015)
  • 著者名/発表者名: Kodai Hashimoto, Hiroshi Unno
  • 雑誌名: Proceedings of SAS 2015, LNCS 巻: 9291 ページ: 199-216
  • DOI: 10.1007/978-3-662-48288-9_12
  • ISBN: 9783662482872, 9783662482889
  • 査読あり / 謝辞記載あり
• [雑誌論文] Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs (2015)
  • 著者名/発表者名: Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
  • 雑誌名: Proceedings of APLAS 2015, LNCS 巻: 9458 ページ: 295-312
  • DOI: 10.1007/978-3-319-26529-2_16
  • ISBN: 9783319265285, 9783319265292
  • 査読あり / 謝辞記載あり
• [雑誌論文] Verification of Tree-Processing Programs via Higher-Order Mode Checking (2015)
  • 著者名/発表者名: Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
  • 雑誌名: Mathematical Structures in Computer Science 巻: Volume 25, Special Issue 04 号: 4 ページ: 841-866
  • DOI: 10.1017/s0960129513000054
  • 査読あり
• [雑誌論文] 高階木変換器の自動検証のための反例発見と抽象化改良 (2015)
  • 著者名/発表者名: 松本雄磨, 小林直樹, 海野広志
  • 雑誌名: コンピュータ ソフトウェア 巻: 32 号: 1 ページ: 1_161-1_178
  • DOI: 10.11309/jssst.32.1_161
  • NAID: 130004892316
  • ISSN: 0289-6540
  • 査読あり / 謝辞記載あり
• [雑誌論文] Inferring Simple Solutions to Recursion-free Horn Clauses via Sampling (2015)
  • 著者名/発表者名: Hiroshi Unno, Tachio Terauchi.
  • 雑誌名: Proceedings of TACAS 2015, LNCS 巻: 9035 ページ: 149-163
  • DOI: 10.1007/978-3-662-46681-0_10
  • ISBN: 9783662466803, 9783662466810
  • 査読あり / 謝辞記載あり
• [雑誌論文] Relaxed Stratication: A New Approach to Practical Complete Predicate Refinement (2015)
  • 著者名/発表者名: Tachio Terauchi, Hiroshi Unno
  • 雑誌名: Proceedings of ESOP 2015, LNCS 巻: 9032 ページ: 610-633
  • DOI: 10.1007/978-3-662-46669-8_25
  • ISBN: 9783662466681, 9783662466698
  • 査読あり / 謝辞記載あり
• [雑誌論文] Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs (2015)
  • 著者名/発表者名: Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
  • 雑誌名: Proceedings of CAV 2015, LNCS 巻: 未定
  • 査読あり / 謝辞記載あり
• [雑誌論文] Automatic Termination Verification for Higher-Order Functional Programs (2014)
  • 著者名/発表者名: Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
  • 雑誌名: Proceedings of ESOP 2014, LNCS 巻: 8410 ページ: 392-411
  • DOI: 10.1007/978-3-642-54833-8_21
  • ISBN: 9783642548321, 9783642548338
  • 査読あり / 謝辞記載あり
• [雑誌論文] 高階木変換器の自動検証のための反例発見と抽象化改良 (2014)
  • 著者名/発表者名: 松本 雄磨, 小林 直樹, 海野 広志
  • 雑誌名: 第 16 回プログラミングおよびプログラミング言語ワークショップ予稿集 巻: - ページ: 1-18
  • NAID: 130004892316
  • 査読あり
• [学会発表] Refinement Caml: A Refinement Type Checking and Inference Tool for OCaml (2016)
  • 著者名/発表者名: Hiroshi Unno
  • 学会等名: Dagstuhl Seminar on Language Based Verification Tools for Functional Programs
  • 発表場所: Wadern, Germany
  • 年月日: 2016-03-31
  • 国際学会
• [学会発表] Relational Verification of Functional Programs via Induction-based Horn Constraint Solving (2016)
  • 著者名/発表者名: Hiroshi Unno
  • 学会等名: NII Shonan Meeting on Higher-Order Model Checking
  • 発表場所: 湘南国際村センター（神奈川県三浦郡）
  • 年月日: 2016-03-19
  • 国際学会
• [学会発表] Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types (2015)
  • 著者名/発表者名: Hiroshi Unno
  • 学会等名: NII Shonan Meeting on Semantics and Verification of Object-Oriented Languages
  • 発表場所: 湘南国際村センター（神奈川県三浦郡）
  • 年月日: 2015-09-21
  • 国際学会
• [学会発表] Automating Well-Founded Induction for Horn Clause Solving (2015)
  • 著者名/発表者名: Sho Torii
  • 学会等名: 日本ソフトウェア科学会第32 回大会
  • 発表場所: 早稲田大学（東京都新宿区）
  • 年月日: 2015-09-11
• [学会発表] Higher-order Program Verification as Renement Type Inference (2015)
  • 著者名/発表者名: Hiroshi Unno
  • 学会等名: Workshop on Higher- Order Program Analysis (HOPA 2015)
  • 発表場所: 京都大学（京都府京都市）
  • 年月日: 2015-07-04
  • 国際学会 / 招待講演
• [学会発表] Automating Relatively Complete Verification of Higher-order Functional Programs (2013)
  • 著者名/発表者名: 海野 広志
  • 学会等名: 日本ソフトウェア科学会創設30周年記念大会
  • 発表場所: 東京
  • 招待講演
• [備考]
  • URL: http://www.cs.tsukuba.ac.jp/~uhiro/