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

量的情報流の正確な検証

研究課題

研究課題/領域番号 23700026
研究種目

若手研究(B)

配分区分基金
研究分野 ソフトウエア
研究機関名古屋大学

研究代表者

寺内 多智弘  名古屋大学, 情報科学研究科, 准教授 (70447150)

研究期間 (年度) 2011 – 2013
研究課題ステータス 完了 (2013年度)
配分額 *注記
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2013年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2012年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2011年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
キーワードセキュリティ / プログラミング言語 / プログラム検証 / 量的情報流 / 情報セキュリティ / プログラム解析 / ソフトウェアモデル検査
研究概要

量的情報流の困難性に関する研究を行い、beliefやmin entropy channel capacityなど様々な情報理論的尺度に基づく量的情報流に関する検証・推論問題の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も考察した。また、ソフトウェアモデル検査技術と#SATソルバ等カウンティングアルゴリズムを応用した高精度な量的情報流上限検証・推論アルゴリズムを提案した。また、検証アルゴリズムの基礎となるソフトウェアモデル検査技術の改良に関する研究を行った。

報告書

(4件)
  • 2013 実績報告書   研究成果報告書 ( PDF )
  • 2012 実施状況報告書
  • 2011 実施状況報告書

研究成果

(27件)

すべて 2014 2013 2012 2011

すべて 雑誌論文 学会発表

  • [雑誌論文] Automatic Termination Verification for Higher-Order Functional Programs2014

    • 著者名/発表者名
      Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
    • 雑誌名

      Proceedings of the 23rd European Symposium on Programming (ESOP 2014), Lecture Notes in Computer Science

      巻: 8410 ページ: 392-411

    • DOI
      10.1007/978-3-642-54833-8_21
    • 関連する報告書
      2013 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Quantitative Information Flow as Safety and Liveness Hyperproperties2014

    • 著者名/発表者名
      Hirotoshi Yasuoka and Tachio Terauchi
    • 雑誌名

      Theoretical Computer Science

      巻: - ページ: 167-182

    • DOI
      10.1016/j.tcs.2013.07.031
    • 関連する報告書
      2013 実績報告書
    • 査読あり / 謝辞記載あり
  • [雑誌論文] Automating Relatively Complete Verification of Higher-Order Functional Programs. In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013)2013

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
    • 雑誌名

      ACM SIGPLAN Notices

      巻: 48(1) ページ: 75-86

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて2013

    • 著者名/発表者名
      岩塚卓也,寺内多智弘,結縁祥治
    • 雑誌名

      情報処理学会論文誌 : プログラミング(PRO)

      巻: 6(3)

    • NAID
      110009656444
    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] 無限小定数と限量子除去法によるハイブリッドシステムの検証に向けて2013

    • 著者名/発表者名
      岩塚卓弥, 寺内多智弘, 結縁祥治
    • 雑誌名

      情報処理学会論文誌プログラミング(PRO)

      巻: 6(3) ページ: 20-32

    • NAID
      110009656444
    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Automating Relatively Complete Verification of Higher-order Functional Programs2013

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
    • 雑誌名

      Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13), ACM

      巻: - ページ: 75-86

    • DOI
      10.1145/2429069.2429081
    • 関連する報告書
      2012 実施状況報告書
    • 査読あり
  • [雑誌論文] Automated Verification of Higher-order Functional Programs2013

    • 著者名/発表者名
      Tachio Terauchi
    • 雑誌名

      Proceeings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science, Springer

      巻: 7294 ページ: 2-2

    • DOI
      10.1007/978-3-642-29822-6_2
    • 関連する報告書
      2012 実施状況報告書
  • [雑誌論文] Quantitative Information Flow as Safety and Liveness Hyperproperties. In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012)2012

    • 著者名/発表者名
      Hirotoshi Yasuoka and Tachio Terauchi
    • 雑誌名

      Electronic Proceedings in Theoretical Computer Science

      巻: 85 ページ: 77-91

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] Quantitative Information Flow as Safety and Liveness Hyperproperties2012

    • 著者名/発表者名
      Hirotoshi Yasuoka, Tachio Terauchi
    • 雑誌名

      Proceedings of the 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012), Electronic Proceedings in Theoretical Computer Science

      巻: 85 ページ: 77-91

    • DOI
      10.4204/eptcs.85.6
    • 関連する報告書
      2012 実施状況報告書
    • 査読あり
  • [雑誌論文] On Bounding Problems of Quantitative Information Flow2011

    • 著者名/発表者名
      Hirotoshi Yasuoka and Tachio Terauchi
    • 雑誌名

      Journal of Computer Security

      巻: 19.6 ページ: 1029-1082

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] On bounding problems of quantitative information flow2011

    • 著者名/発表者名
      Hirotoshi Yasuoka, Tachio Terauchi
    • 雑誌名

      Journal of Computer Security

      巻: 19 ページ: 1029-1082

    • DOI
      10.3233/jcs-2011-0437
    • 関連する報告書
      2011 実施状況報告書
    • 査読あり
  • [学会発表] Automatic Termination Verification for Higher-Order Functional Programs2014

    • 著者名/発表者名
      Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
    • 学会等名
      ソフトウェア科学会 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Automatic Termination Verification for Higher-Order Functional Programs2014

    • 著者名/発表者名
      Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
    • 学会等名
      The 23rd European Symposium on Programming (ESOP 2014)
    • 発表場所
      Grenoble, France
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Automatic Termination Verification for Higher-Order Functional Programs2014

    • 著者名/発表者名
      Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi
    • 学会等名
      ソフトウェア科学会 第16回プログラミングおよびプログラミング言語ワークショ ップ (PPL 2014)
    • 発表場所
      熊本県阿蘇市
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Automating Relatively Complete Verification of Higher-Order Functional Programs2013

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi
    • 学会等名
      ソフトウェア科学会 第15回プログラミ ングおよびプログラミング言語ワークショップ (PPL 2013)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 無限小定数と限量子除去法によるハイブリッドシステムの検証2013

    • 著者名/発表者名
      岩塚卓也,寺内多智弘,結縁祥治
    • 学会等名
      情報処理学会 第93回プログラミング研究会
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Automating Relatively Complete Verification of Higher-order Functional Programs2013

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
    • 学会等名
      日本ソフトウェア科学界第15回プログラミングおよびプログラミング言語ワークショップ(PPL2013)
    • 発表場所
      福島県会津若松 東山温泉 御宿東鳳
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] 無限小定数と限量子除去法によるハイブリッドシステムの検証2013

    • 著者名/発表者名
      岩塚卓弥, 寺内多智弘, 結縁祥治
    • 学会等名
      情報処理学会プログラミング研究会
    • 発表場所
      国立情報学研究所
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] Automating Relatively Complete Verification of Higher-order Functional Programs2013

    • 著者名/発表者名
      Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
    • 学会等名
      The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)
    • 発表場所
      Rome, Italy
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] On Complexity of Verifying Quantitative Information Flow2012

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      Dagstuhl Seminar 12481 : Quantitative Security Analysis
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Automated Verification of Higher-Order Functional Programs2012

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      Proceedings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science 7294
    • 発表場所
      (pp.2. Springer)
    • 関連する報告書
      2013 研究成果報告書
    • 招待講演
  • [学会発表] On Complexity of Verifying Quantitative Information Flow2012

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      Dagstuhl Seminar 12481: Quantitative Security Analsysis
    • 発表場所
      Dagstuhl, Germany
    • 関連する報告書
      2012 実施状況報告書
    • 招待講演
  • [学会発表] Automated Verification of Higher-order Functional Programs2012

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      The 11th International Symposium on Functional and Logic Programming (FLOPS 2012)
    • 発表場所
      神戸大学
    • 関連する報告書
      2012 実施状況報告書
    • 招待講演
  • [学会発表] Quantitative Information Flow as Safety and Liveness Hyperproperties2012

    • 著者名/発表者名
      Hirotoshi Yasuoka, Tachio Terauchi
    • 学会等名
      The 10th Workshop on Quantitative Aspects of Programming Language and Systems (QAPL 2012)
    • 発表場所
      Tallinn, Estonia
    • 関連する報告書
      2012 実施状況報告書
  • [学会発表] Relatively Complete Refinement Types from Counterexamples2011

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      NII Shonan Meeting Seminar 005 : Automated Techniques for Higher-Order Program Verification
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Thread-based code cloning for light-weight context sensitive static race detection2011

    • 著者名/発表者名
      Toshiyuki Manabe, Tachio Terauchi
    • 学会等名
      4th NSFC-JSPS workshop on Formal Methods
    • 発表場所
      奈良
    • 関連する報告書
      2011 実施状況報告書
  • [学会発表] Relatively Complete Type System for Higher-order Programs2011

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      NII Shonan Meeting on Automated Techniques for Higher-order Program Verification
    • 発表場所
      神奈川
    • 関連する報告書
      2011 実施状況報告書

URL: 

公開日: 2011-08-05   更新日: 2019-07-29  

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

Powered by NII kakenhi