• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2016 年度 実績報告書

高レベル言語で記述されたソフトウェアの時相的・関係的仕様の検証

研究課題

研究課題/領域番号 16H05856
研究機関筑波大学

研究代表者

海野 広志  筑波大学, システム情報系, 助教 (80569575)

研究期間 (年度) 2016-04-01 – 2020-03-31
キーワードリファインメント型 / 依存型 / 関係的仕様 / 時相的仕様 / ホーン節制約解消 / プログラム検証 / 帰納的定理証明
研究実績の概要

本研究では、研究代表者がこれまでに研究・開発を行ってきた高レベル言語のための検証理論であるリファインメント型システムおよびホーン節制約解消法、関数型言語 OCaml のための全自動・高精度検証ツールである RCaml を発展させ、実用上重要であるにも関わらず既存手法では十分に扱えなかった言語機能(再帰データ構造・参照セル・オブジェクト・モジュール機構・例外処理機構・マルチスレッド機構)および仕様(時相的仕様・関係的仕様)の全自動・高精度検証法の確立を目指している。本年度は以下の成果を得た。
1.再帰データ構造を扱うプログラムを高精度に検証できるようリファインメント型システムを拡張した上で、再帰データ構造によるオブジェクトのエンコード法を考案・実装することによって、オブジェクトを扱うプログラムの高精度検証を実現した。さらに、ホーン節制約解消法を代数データ構造を扱えるよう拡張することによって、拡張された型システムのための型推論を実現し、全自動・高精度検証を可能とした。
2. 無交代様相μ計算の論理式として記述された時相的仕様の検証のために、論理式と検証対象の高レベルプログラムの積をとることによって得られる無限状態 Buechi ゲームを、RCaml が扱える停止性・非停止性検証問題に帰着して解く手法を考案・実装した。
3. 高レベルプログラムの関係的仕様検証のため、帰納的定理証明に基づくホーン節制約解消法を拡張して、ヒープ制約の解消、関係的プログラム合成、余帰納法の自動化を実現した。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

研究実績の概要で述べたとおり、リファインメント型システムおよびホーン節制約解消法の拡張の柱となる部分については順調に進展している。一方、本年度中の実施を予定していた、例外処理機構・マルチスレッド機構の再帰データ構造を用いたエンコード法の確立や、一般の様相μ計算の論理式として記述された時相的仕様の検証といった発展的な研究については当初の計画より遅れている。その理由は平成29年度以降に実施を予定していた関係的仕様検証のための拡張を前倒しして実施したためであり、そちらに関してはシステム検証に関するトップ会議であるCAVに論文が採択されるなど顕著な成果が得られている。

今後の研究の推進方策

現在までの進捗状況で述べたように、平成28年度中に実施を予定していた研究計画と平成29年度以降に予定していた計画が一部入れ替わってはいるが、今後も予定通り研究を推進していく。

  • 研究成果

    (6件)

すべて 2017 2016 その他

すべて 国際共同研究 (2件) 雑誌論文 (1件) (うち査読あり 1件、 謝辞記載あり 1件) 学会発表 (3件)

  • [国際共同研究] Verimag(France)

    • 国名
      フランス
    • 外国機関名
      Verimag
  • [国際共同研究] Yale University(米国)

    • 国名
      米国
    • 外国機関名
      Yale University
  • [雑誌論文] Automating Induction for Solving Horn Clauses2017

    • 著者名/発表者名
      Hiroshi Unno, Sho Torii, Hiroki Sakamoto
    • 雑誌名

      Proceedings of CAV 2017, LNCS

      巻: 印刷中 ページ: 印刷中

    • 査読あり / 謝辞記載あり
  • [学会発表] A Horn Constraint Solver based on Inductive Theorem Proving(ポスター発表)2017

    • 著者名/発表者名
      Hiroki Sakamoto, Sho Torii, Shu Nakao, Hiroshi Unno
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)
    • 発表場所
      華やぎの章 慶山(山梨県笛吹市)
    • 年月日
      2017-03-09 – 2017-03-09
  • [学会発表] Temporal Logics for Higher-Order Functional Programs based on Trace Semantics(ポスター発表)2017

    • 著者名/発表者名
      Yuki Satake, Hiroshi Unno
    • 学会等名
      第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)
    • 発表場所
      華やぎの章 慶山(山梨県笛吹市)
    • 年月日
      2017-03-08 – 2017-03-08
  • [学会発表] Temporal Dependent Contracts for Higher-Order Functions2016

    • 著者名/発表者名
      佐竹 佑規, 海野 広志
    • 学会等名
      日本ソフトウェア科学会第33回大会
    • 発表場所
      東北大学(宮城県仙台市)
    • 年月日
      2016-09-08 – 2016-09-08

URL: 

公開日: 2018-01-16   更新日: 2022-01-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi