课题基金 / 基金详情

Advancement and Application of Type Theory for Improving Software Safety

Advancement and Application of Type Theory for Improving Software Safety
提高软件安全性的类型论进展及应用
批准号：
20240001
负责人：
KOBAYASHI Naoki
金额：
$31.53万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (A)
财政年份：
2008
资助国家：
日本
项目状态：
已结题
起止时间：
2008 至 2010
来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20240001/
关键词：
ソフトウェア検証型システム高階モデル検査資源使用法検証プログラム解析型理論述語抽象化メモリ使用法解析モデル検査高階再帰スキーム資源使用法解析ツリーオートマトン

项目摘要

项目成果

KOBAYASHI Naoki的其他基金

相似基金

相关文献

中文摘要
翻译
本研究项目旨在通过改进我们以前研究过的基于类型的程序验证方法以及发明新的程序验证技术来提高计算机软件的可靠性。在前面的研究中，我们构建了C程序和加密协议的验证工具。在后一项研究中，我们展示了高阶模型检查在程序验证中的新应用，并构建了世界上第一个高阶模型检查器。
英文摘要
This research project aimed to improve the reliability of computer software, by refining type-based program verification methods we have studied before, and also by inventing new program verification techniques. As the former study, we have constructed verification tools for C programs and cryptographic protocols. As the latter study, we have shown novel applications of higher-order model checking to program verification, and constructed the first higher-order model checker in the world.
期刊论文(49)
专著(0)
科研奖励(0)
会议论文
Polymorphic Contracts
多态合约
DOI： --
发表时间： 2010
期刊： Proceedings of European Symposium on Programming (ESOP2011)
影响因子： --
作者： [Joao Filipe Belo, Michael Greenberg, Atsushi Igarashi, Benjamin C.Pierce]
通讯作者： Benjamin C.Pierce
Recursion Schemes for Verification of Higher-Order Programs
用于验证高阶程序的递归方案
DOI： --
发表时间： 2009
期刊： Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on principles of Programming Languages (POPL 2009)
影响因子： --
作者： [Naoki Kobayashi, Types and Higher-Order]
通讯作者： Types and Higher-Order
Substructural Type Systems for Program Analysis
用于程序分析的子结构类型系统
DOI： --
发表时间： 2008
期刊：
影响因子： --
作者： [Eijiro Sumii, Benjamin C.Pierce, Naoki Kobayashi]
通讯作者： Naoki Kobayashi
A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes
DOI： 10.1109/lics.2009.29
发表时间： 2009-08
期刊： 2009 24th Annual IEEE Symposium on Logic In Computer Science
影响因子： --
作者： [N. Kobayashi;C. Ong]
通讯作者： N. Kobayashi;C. Ong
共 26 条
    Study on food oral processing of the elderly by fragment-size analysis
    • 批准号：
      18K02248
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $1.0万
    • 财政年份：
      2018
    • 负责人：
      KOBAYASHI Naoki
    • 依托单位：
      Nihon University
    Regulation mechanisms of lymphocyte trafficking by sphingosine 1-phosphate (S1P) transporters
    • 批准号：
      17K08399
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $3.08万
    • 财政年份：
      2017
    • 负责人：
      KOBAYASHI Naoki
    • 依托单位：
      Setsunan University
    Quantification for food mastication and swallowing using by fragment-size distribution
    • 批准号：
      15K00797
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $1.58万
    • 财政年份：
      2015
    • 负责人：
      KOBAYASHI Naoki
    • 依托单位：
      Nihon University
    On the relation between food fragment distribution and bolus rheology
    • 批准号：
      25750030
    • 项目类别：
      Grant-in-Aid for Young Scientists (B)
    • 资助金额：
      $1.08万
    • 财政年份：
      2013
    • 负责人：
      KOBAYASHI Naoki
    • 依托单位：
      Nihon University
    海外基金