Verifying safety properties of embedded assembly program using innovative software model checking

使用创新的软件模型检查验证嵌入式装配程序的安全属性

• 批准号: 15K00093
• 负责人: YAMANE SATOSHI
• 金额: $ 2.91万
• 依托单位: Kanazawa University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-01 至 2018-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00093/
• 关键词: ソフトウェアモデル検査; 組込みアセンブリプログラム; 抽象化精錬; ＳＭＴ; 定理証明; 動的プログラム解析; SMT; プログラム解析

项目成果

LogChamber: Inferring Source Code Locations Corresponding to Mobile Applications Run-time Logs

LogChamber：推断与移动应用程序运行时日志对应的源代码位置

• DOI: 10.2197/ipsjjip.24.700
• 发表时间: 2016
• 期刊: Journal of Information Processing
• 作者: Yuki Ono;Kouhei Sakurai;Satoshi Yamane
• 通讯作者: Satoshi Yamane

Formal Verification of Dynamically Reconfigurable Systems

动态可重构系统的形式化验证

• 发表时间: 2015
• 期刊: 2015 IEEE 4th Global Conference on Consumer Electronics (GCCE 2015)
• 作者: R.Yanase;T.Sakai,M.Sakai,S.Yaname
• 通讯作者: T.Sakai,M.Sakai,S.Yaname

定理証明器Princess を用いた組込みアセンブリプログラムのリアルタイム安全性の演繹的検証

使用 Princess 定理证明器对嵌入式汇编程序实时安全性进行演绎验证

• 发表时间: 2018
• 期刊: MSS2017-84
• 作者: 小田島直樹;福田岳飛;山根智
• 通讯作者: 山根智

組込みアセンブリプログラムのリアルタイム性の検証手法 ～ 組込みプログラムのためのモデル検査と演繹的検証 ～

嵌入式汇编程序实时性能验证方法-嵌入式程序的模型检验与演绎验证-

• 发表时间: 2017
• 期刊: MSS2016-83
• 作者: 上里 友弥;南出 靖彦;山根智
• 通讯作者: 山根智

Integration of Supervised and Unsupervised Learning for Deep Neural Network

深度神经网络监督学习和无监督学习的集成

• 发表时间: 2016
• 作者: Takafumi Uchiyama;Takio Kurita;Satoshi Yamane and Kohei Sakurai
• 通讯作者: Satoshi Yamane and Kohei Sakurai