课题基金 / 基金详情

Program Verification Based on Higher-Order Fixpoint Logic

Program Verification Based on Higher-Order Fixpoint Logic
基于高阶不动点逻辑的程序验证
批准号：
20H00577
负责人：
小林 直樹
金额：
$28.45万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (A)
财政年份：
2020
资助国家：
日本
项目状态：
已结题
起止时间：
2020-04-01 至 2021-03-31
来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20H00577/
关键词：
プログラム検証高階不動点論理確率付き高階不動点論理モデル検査高階モデル検査

项目摘要

项目成果

小林 直樹的其他基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
様々な重要な社会基盤がコンピュータによって制御されている今日，ソフトウェアが期待通りの動作をすることを保証するためのプログラム検証技術は今後ますます重要になる．我々はシステム検証技術の主流であるモデル検査の真の拡張である高階モデル検査とそれに基づくプログラム検証手法について世界をリードしてきたが，最近になって高階モデル検査の中でも高階不動点論理に基づく方式が特に有望であることを見出した．そこで本研究では高階不動点論理に基づくプログラム検証の理論をさらに発展させるとともに，他の関連する理論・技術と組み合わせることによって，高階モデル検査に基づくプログラム自動検証手法を実用レベルにまで昇華させることを目指した．採択後数か月で廃止になったため、上記目的の達成には至っていないが、これまでに以下の研究を行った。まず、最大不動点のみを持つ高階不動点論理に整数を加えて拡張したνHFL(Z)の論理式の真偽値判定手法として、(1) 述語抽象化と高階モデル検査を組み合わせる方式、(2)詳細型システムにおける型推論問題に帰着する方式、の2種類について並行して研究を進め、両者に基づくνHFL(Z)の論理式の自動真偽値判定ツールPaHFLおよびRetHFLを構築した。さらにそれらのツールをプログラムの自動検証に応用し、既存の同目的のツールHorusよりも優れた性能を示すことを確認した。また、前年度から取り組んでいた高階不動点論理に確率を加えて拡張した確率付き高階不動点論理PHFLの研究を継続し、PHFLモデル検査問題の困難性を解析階層（analytical hierarchy)を用いて特徴づけるとともに、型システムを用いて決定可能な部分クラスを与えた。
期刊论文(3)
专著(0)
科研奖励(0)
会议论文
A Probabilistic Higher-Order Fixpoint Logic
概率高阶不动点逻辑
DOI： --
发表时间： 2020
期刊： Proceedings of FSCD 2020, LIPIcs
影响因子： --
作者： [Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada]
通讯作者： and Takeshi Tsukada
Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking
用于 nuHFL(Z) 有效性检查的谓词抽象和 CEGAR
DOI： --
发表时间： 2020
期刊： Proceedings of SAS 2020, Springer LNCS
影响因子： --
作者： [Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki and Takeshi Tsukada]
通讯作者： Ryota Suzuki and Takeshi Tsukada
A New Refinement Type System for Automated nu-HFLZ Validity Checking
用于自动 nu-HFLZ 有效性检查的新型细化系统
DOI： --
发表时间： 2020
期刊： Proceedings of APLAS 2020, Springer LNCS
影响因子： --
作者： [Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, and Takeshi Tsukada]
通讯作者： and Takeshi Tsukada
無住道暁と南宋代成立典籍に関する総合的研究
  • 批准号：
    23K00298
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $1.41万
  • 财政年份：
    2023
  • 负责人：
    小林 直樹
  • 依托单位：
    Osaka Metropolitan University
潜在的カビ毒産生菌種を利用したカビ毒生合成抑制メカニズムの解明
  • 批准号：
    23K05081
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $2.91万
  • 财政年份：
    2023
  • 负责人：
    小林 直樹
  • 依托单位：
    Azabu University
偏光分光型マルチスペクトルカメラを用いた目視診断用画像システムの研究開発
  • 批准号：
    23K11878
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $3.08万
  • 财政年份：
    2023
  • 负责人：
    小林 直樹
  • 依托单位：
    Saitama Medical University
Program Verification Techniques for the AI Era
  • 批准号：
    20H05703
  • 项目类别：
    Grant-in-Aid for Scientific Research (S)
  • 资助金额：
    $121.8万
  • 财政年份：
    2020
  • 负责人：
    小林 直樹
  • 依托单位：
    The University of Tokyo