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

2015 Fiscal Year Research-status Report

分離論理を用いたソフトウェア検証の基礎理論

Research Project

Project/Area Number 15K00027
Research InstitutionNational Institute of Informatics

Principal Investigator

龍田 真  国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)

Project Period (FY) 2015-04-01 – 2018-03-31
Keywordsソフトウェア検証 / 数理論理 / 分離論理
Outline of Annual Research Achievements

一般的帰納的定義}の条件で次の(1)(2)を満たすものを発見し、その性質を証明する研究を行った。(1) 記号ヒープ体系にその条件下の一般的帰納的定義を追加しても、エンテイルメントの真偽が決定可能である, (2) リストセグメントなどのよく使用される基本的なデータ構造が記述できる. 本研究の実用的な意義は、メモリーエラーを自動定理証明により検証する方法に対して、リストセグメントのようなよく使われる基本的なデータ構造を扱うプログラムを対話的入力なしに全自動で検証できる方法をはじめて与えることである。
平成27年度の実績は次のようである。論文 Iosif et al 2013の証明の条件を吟味し、その条件を緩めて、データフィールドを扱えるようにした。単項二階論理への翻訳を可能とする条件として、単項帰納的定義の条件を発見した。この条件を用いて、エンテイルメントの決定手続きを設計し決定可能性定理を証明した。このシステムのパソコンへ実装した。

Current Status of Research Progress
Current Status of Research Progress

1: Research has progressed more than it was originally planned.

Reason

平成27年度にやるように当初計画していたことは全て達成できた。また、bounded treewidth の条件下で循環証明体系を構築し、その決定可能性を証明した。また、その実装も開始した。以上から進捗状況はよいといえる。

Strategy for Future Research Activity

(1) 平成27年度に構成した検証システムの決定手続きのパソコン上への実装を完成する。実装は、O'Hearn らのグループの 2005, 2006年の論文をはじめとする分離論理の検証システムの実装の論文のアイデアを参考にして、検証システムのプロトタイプを作成する。(2) 実装した検証システムに, ベンチマークなどを走らせ実験する。(3) 平成27年度に発見した条件と理論をさらに洗練する。
検証システムの実装および実験のために、平成28年度には研究補助者を週1日雇用する。最新の状況を捉えるために、成果発表とは別に年1回トップ会議に出席して情報収集する。国内の関連した研究を行っているグループを訪問し、途中の成果を発表し、研究討論を行ってフィードバックを得る。研究成果を権威ある国際会議で発表し研究討論を行う。

Causes of Carryover

実装および実験のための研究補助の支出のため追加交付を受けたが、発表旅費が予定より少なかったため次年度使用額が生じた。

Expenditure Plan for Carryover Budget

理論研究が予定よりよく進み、また実験から得るデータが予想より研究に役立つことがわかったため、実装とそのシステムによる実験にも重きを置くこととし、そのために研究員または研究補助員を雇用する。その他の点については当初予定通り進める。

  • Research Products

    (4 results)

All 2016 2015

All Journal Article (3 results) (of which Peer Reviewed: 3 results) Presentation (1 results) (of which Int'l Joint Research: 1 results)

  • [Journal Article] Completeness for Recursive Procedures in Separation Logic2016

    • Author(s)
      Mahmudul Faisal Al Ameen and Makoto Tatsuta
    • Journal Title

      Theoretical Computer Science

      Volume: 631 Pages: 73--96

    • DOI

      10.1016/j.tcs.2016.04.004

    • Peer Reviewed
  • [Journal Article] Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic2016

    • Author(s)
      Makoto Tatsuta and Daisuke Kimura
    • Journal Title

      Proceedings of the 18th JSSST Workshop on Programming and Programming Languages

      Volume: 1 Pages: 1--15

    • Peer Reviewed
  • [Journal Article] Separation Logic with Monadic Inductive Definitions and Implicit Existentials2015

    • Author(s)
      Makoto Tatsuta and Daisuke Kimura
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 9458 Pages: 69--89

    • Peer Reviewed
  • [Presentation] Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions2015

    • Author(s)
      Makoto Tatsuta and Daisuke Kimura
    • Organizer
      Continuity, Computability, Constructivity: From Logic to Algorithms (CCC2015)
    • Place of Presentation
      Kochel, Germany
    • Year and Date
      2015-09-16 – 2015-09-16
    • Int'l Joint Research

URL: 

Published: 2017-01-06  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi