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

2017 年度 実績報告書

ビッグデータ処理の形式検証に向けて

研究課題

研究課題/領域番号 15K12013
研究機関国立研究開発法人産業技術総合研究所

研究代表者

Affeldt Reynald  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (40415641)

研究分担者 田中 哲  国立研究開発法人産業技術総合研究所, 情報・人間工学領域, 主任研究員 (10357452)
J Garrigue  名古屋大学, 多元数理科学研究科, 准教授 (80273530)
研究期間 (年度) 2015-04-01 – 2018-03-31
キーワード定理証明支援系 / 簡潔データ構造 / プログラミング言語C / コード生成器
研究実績の概要

平成29年度、昨年度提案したコード生成の手法を実用的な応用に適用し、簡潔データ構造の基礎の形式化を拡張した。平成28年度に提案したコード生成の手法(monomorphizationというプログラム変換に基づくC言語のコード生成器とmonadificationというプログラム変換器)の開発を進め、応用例に適用した。特に、平成27年度に形式検証したrankアルゴリズムに適用した。その結果として、C言語のコードで記述された実用的な実装を得られ、その正しさもmonadという概念を用いて確認した。また、同じmonadの概念を用いて、正しさ以外の性質(計算量など)も形式的に検証できた。以上の生成器と変換器は定理証明支援系Coqのプラグインとして実現しており、これをオープンソースコードとして配布した。その成果を国内ワークショップで発表し、雑誌論文として投稿し、採択され、招待講演として国際ワークショプで発表した。また、上記のコード生成器を最適化で拡張した。具体的には、C言語で記述された実装の効率改善のため、linearity解析を実装した。また、平成27年度で開始した簡潔データ構造の基礎の形式化を拡張した。具体的には、select関数とその性質およびLOUDS木という代表的な簡潔データ構造とその性質を形式化した。以上のlinearity解析による最適化
と簡潔データ構造の形式化を国内ワークショップでポスターとして発表した。

  • 研究成果

    (10件)

すべて 2018 2017 その他

すべて 雑誌論文 (1件) (うち国際共著 1件、 査読あり 1件、 オープンアクセス 1件) 学会発表 (7件) (うち国際学会 1件、 招待講演 1件) 備考 (2件)

  • [雑誌論文] Safe Low-level Code Generation in Coq Using Monomorphization and Monadification2018

    • 著者名/発表者名
      Tanaka Akira、Affeldt Reynald、Garrigue Jacques
    • 雑誌名

      Journal of Information Processing

      巻: 26 ページ: 54~72

    • DOI

      https://doi.org/10.2197/ipsjjip.26.54

    • 査読あり / オープンアクセス / 国際共著
  • [学会発表] Safe Low-level Code Generation in Coq using Monomorphization and Monadification2017

    • 著者名/発表者名
      田中 哲,Reynald Affeldt,Jacques Garrigue
    • 学会等名
      情報処理学会プログラミング研究会 第114回プログラミング研究発表会
  • [学会発表] Coq からの低レベル C コード生成2017

    • 著者名/発表者名
      田中哲
    • 学会等名
      The 13th Theorem Proving and Provers Meeting (TPP 2017)
  • [学会発表] 形式的な情報・符号理論のライブラリに向けて2017

    • 著者名/発表者名
      Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
    • 学会等名
      The 13th Theorem Proving and Provers Meeting (TPP 2017)
  • [学会発表] Generation of Code from Coq for Succinct Data Structures2017

    • 著者名/発表者名
      Reynald Affeldt
    • 学会等名
      ENabling TRust through Os Proofs...and beYond (ENTROPY 2018)
    • 国際学会 / 招待講演
  • [学会発表] Coqによる簡潔データ構造のライブラリに向けての今後の課題2017

    • 著者名/発表者名
      田中 哲, Reynald Affeldt, Jacques Garrigue
    • 学会等名
      第20回プログラミングおよびプログラミング言語ワークショップ(PPL2018)
  • [学会発表] Ruby Extension Library Verified using Coq Proof-assistant2017

    • 著者名/発表者名
      田中哲
    • 学会等名
      RubyKaigi 2017
  • [学会発表] Coq からの C プログラム生成2017

    • 著者名/発表者名
      田中哲
    • 学会等名
      Proof Summit 2017
  • [備考] https://staff.aist.go.jp/tanaka-akira/succinct/

  • [備考] https://github.com/affeldt-aist/infotheo

URL: 

公開日: 2018-12-17  

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

Powered by NII kakenhi