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

高階関数型言語のためのソフトウェアモデル検査

Research Project

Project/Area Number 12J08057
Research Category

Grant-in-Aid for JSPS Fellows

Allocation TypeSingle-year Grants
Section国内
Research Field Software
Research InstitutionThe University of Tokyo (2013)
Tohoku University (2012)

Principal Investigator

佐藤 亮介  東京大学, 大学院情報理工学系研究科, 特別研究員(PD)

Project Period (FY) 2012 – 2013
Project Status Completed (Fiscal Year 2013)
Budget Amount *help
¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 2013: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2012: ¥1,000,000 (Direct Cost: ¥1,000,000)
Keywords高階関数型言語 / 高階モデル検査 / ソフトウェアモデル検査 / 詳細化型 / 継続渡し形式変換 / 述語抽象化
Research Abstract

高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張に関する研究を進め、その成果を論文として投稿した。
検証の枠組みの拡張として、既存の高階関数型言語のための自動検証手法では扱えなかった関数の等価性や単調性などの関数の性質を扱えるようにした。具体的には、このような関数の性質に関する検証問題を既存の検証手法で扱える問題に帰着する方法を提案した。
既存の高階関数型プログラムの自動検証手法のほとんどは、量化子を含まない一階の述語を用いてプログラムを抽象化することによって検証を行っている。しかし、量化子を含まない一階の述語という制限のため、関数の等価性など、全称や関数を用いないと表すことができない性質を扱えなかった。例えば、次のように定義された二つの関数sum、sum2が等しいということが検証できない。
let rec sum n = if n <0 then 0 else n + sum (n-l)
let rec sumacc n m = if n <0 then m el se sumacc (n-1) (n+m)
let sum2 n = sumacc n 0
ここで、sumは1からnまでの整数の和を求める関数であり、sum2はそれを累積変数を用いて求めるものである。
本研究では、このような全称および関数を用いないと表せない性質の検証問題を、既存の一階の述語のみを扱う検証問題に帰着する方法を提案した。
この拡張した検証の枠祖みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器のプロトタイプを実装した。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。ここまでに得られた成果を国内会議の場で発表し、同時に他の研究者との意見交換を行った。

Strategy for Future Research Activity

(抄録なし)

Report

(2 results)
  • 2013 Annual Research Report
  • 2012 Annual Research Report
  • Research Products

    (4 results)

All 2014 2013 2012

All Journal Article (1 results) (of which Peer Reviewed: 1 results) Presentation (3 results)

  • [Journal Article] Towards a scalable software model checker for higher-order programs2013

    • Author(s)
      Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
    • Journal Title

      Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM 2013)

      Volume: - Pages: 56-62

    • DOI

      10.1145/2426890.2426900

    • Related Report
      2012 Annual Research Report
    • Peer Reviewed
  • [Presentation] 一階詳細化を用いた関数型プログラムの関係的性質の検証2014

    • Author(s)
      佐藤亮介
    • Organizer
      第16回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      熊本県(ビラパークホテル)
    • Year and Date
      2014-03-05
    • Related Report
      2013 Annual Research Report
  • [Presentation] Towards a scalable software model checker for higher-order programs2013

    • Author(s)
      Ryosuke Sato
    • Organizer
      ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation (PEPM 2013)、
    • Place of Presentation
      Rome, Italy
    • Year and Date
      2013-01-21
    • Related Report
      2012 Annual Research Report
  • [Presentation] MoCHi: Software Model Checker for a Higher-Order Functional Language2012

    • Author(s)
      Ryosuke Sato
    • Organizer
      ACM SIGPLAN Workshop on ML
    • Place of Presentation
      Copenhagen, Denmark
    • Year and Date
      2012-09-13
    • Related Report
      2012 Annual Research Report

URL: 

Published: 2013-04-25   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi