• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

様相論理に基づいたプログラム解析手法の研究

Research Project

Project/Area Number 15700011
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionKyoto University

Principal Investigator

五十嵐 淳  京都大学, 情報学研究科, 講師 (40323456)

Project Period (FY) 2003 – 2005
Project Status Completed (Fiscal Year 2005)
Budget Amount *help
¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 2005: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2004: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2003: ¥1,000,000 (Direct Cost: ¥1,000,000)
Keywords情報流解析 / 様相論理 / 非干渉性 / 型システム / 論理関係 / メタプログラミング / 直観主義 / 不干渉性 / 線形時間時相論理
Research Abstract

本研究の主な目的は,様々なプログラム解析を統一的に扱える枠組みを,様相論理という論理体系を元にして開発し,実際のプログラミング言語の解析のための型システムとして応用することにある.
本年度は,昨年度まで研究を行ってきた様相論理体系に基づく情報流解析の枠組に関する考察と,論理関係を用いた非干渉性定理の一般化を行った.非干渉性とは,秘匿性の低い計算結果は,秘匿性の高い入力に依存しないこと,すなわち,秘匿性の高い入力の情報が1ビットたりとも漏洩していなことを示す性質であり,情報流解析の正当性として用いられている.従来の多くの研究では,入力と出力に関しては,整数などの基本的データ型に限って非干渉性が考察されてきた.我々の研究では,プログラムの等しさを論理関係というプログラム意味論の分野で使われている技法を用いて定式化することにより,基本的データだけではなく,関数値などの高階なデータ型に関しても適用可能な形に,非干渉性定理を一般化し,それを証明することに成功した.
またこの結果から昨年まで行ってきたDCCという別の情報流解析の枠組との比較についても,両者は,比較不可能(どちらも相手よりも勝っている部分がある)という結論が出た.今後は両者の長所を統合したような,より一般的な情報流解析の枠組を目指すことが望まれる.

Report

(3 results)
  • 2005 Annual Research Report
  • 2004 Annual Research Report
  • 2003 Annual Research Report
  • Research Products

    (8 results)

All 2006 2005 2004 Other

All Journal Article (5 results) Publications (3 results)

  • [Journal Article] Resource Usage Analysis for a Functional Language with Exceptions2006

    • Author(s)
      Futoshi Iwama
    • Journal Title

      Proceedings of PEPM'06

      Pages: 38-47

    • Related Report
      2005 Annual Research Report
  • [Journal Article] 様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明2006

    • Author(s)
      四熊 尚方
    • Journal Title

      PPL2006 予稿集

      Pages: 134-149

    • Related Report
      2005 Annual Research Report
  • [Journal Article] メタプログラミングのための時相論理に基づく型付λ計算2005

    • Author(s)
      湯瀬 芳洋
    • Journal Title

      PPL2005予稿集

      Pages: 57-73

    • Related Report
      2004 Annual Research Report
  • [Journal Article] 例外機構を備えた言語のための資源使用法解析2005

    • Author(s)
      岩間 太
    • Journal Title

      PPL2005予稿集

      Pages: 154-170

    • Related Report
      2004 Annual Research Report
  • [Journal Article] A Modal Foundation of Secure Information Flow2004

    • Author(s)
      Kenji Miyamoto
    • Journal Title

      Proceedings of FCS'04

      Pages: 187-203

    • Related Report
      2004 Annual Research Report
  • [Publications] Masahiko Sato: "Calculi of Meta-variables"Proceedings of CSL'03, LNCS. 2803. 484-497 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Atsushi Igarashi: "Resource Usage Analysis"ACM Trasactions on Programming Languages and Systems. (in press).

    • Related Report
      2003 Annual Research Report
  • [Publications] Atushi Igarashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)

    • Related Report
      2003 Annual Research Report

URL: 

Published: 2003-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi