课题基金 / 基金详情

Model and formal verification of the C language for secure construction of embedded software

Model and formal verification of the C language for secure construction of embedded software
嵌入式软件安全构建的C语言模型与形式化验证
批准号：
24500051
负责人：
AFFELDT Reynald
金额：
$3.24万
依托单位：
National Institute of Advanced Industrial Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2012
资助国家：
日本
项目状态：
已结题
起止时间：
2012-04-01 至 2016-03-31
来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24500051/
关键词：
形式検証C言語アセンブリ言語組込みソフトウェア定理証明支援系Coq多倍長整数演算セキュリティプロトコルTLS詳細化

项目摘要

项目成果

AFFELDT Reynald的其他基金

相似基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
定理証明支援系に基づく形式検証
基于定理证明支持系统的形式化验证
DOI： --
发表时间： 2014
期刊： 情報処理
影响因子： --
作者： [Atsushi Kurokawa, Masayuki Watanabe, Makoto Hoshi, and Masa-aki Fukase, アフェルト レナルド]
通讯作者： アフェルト レナルド
Formal Verification of Low-level Programs
低层程序的形式化验证
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
Coq Coding Sprint参加報告
Coq Coding Sprint 参与报告
DOI： --
发表时间： 2015
期刊：
影响因子： --
作者： [Shinpei Hayashi, Daiki Hoshino, Jumpei Matsuda, Motoshi Saeki, Takayuki Omori, Katsuhisa Maruyama, Masa-aki Fukase and Tomoaki Sato, Reynald Affeldt]
通讯作者： Reynald Affeldt
Proving Properties on Programs
证明程序的性质
DOI： --
发表时间： 2015
期刊：
影响因子： --
作者： [Shinpei Hayashi, Daiki Hoshino, Jumpei Matsuda, Motoshi Saeki, Takayuki Omori, Katsuhisa Maruyama, Masa-aki Fukase and Tomoaki Sato, Reynald Affeldt, 田島香織，丸山勝久, Masa-aki Fukase 他6名, Reynald Affeldt, Reynald Affeldt]
通讯作者： Reynald Affeldt
共 16 条
    Towards formal verification of big data processing
    Formal Proofs of Realistic Programs using Separation Logic
    海外基金