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

A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata

使用动态线性混合自动机动态可重构系统的形式化方法的案例研究

• DOI: 10.1007/978-3-319-47846-3_6
• 发表时间: 2016
• 期刊: Lecture Notes in Computer Science
• 作者: Ryo Yanase;Tatsunori Sakai;Makoto Sakai and Satoshi Yamane
• 通讯作者: Makoto Sakai and Satoshi Yamane

Specification and Verification of Dynamically Reconfigurable Systems using Dynamic Linear Hybrid Automata

使用动态线性混合自动机的动态可重构系统的规范和验证

• DOI: 10.4236/jsea.2016.99030
• 发表时间: 2016
• 期刊: Journal of Software Engineering and Applications
• 作者: R.Yanase;M.Sakai;T.Sakai;S.Yamane
• 通讯作者: S.Yamane

記号実行による組込みアセンブリプログラムのソフトウェアモデル検査

使用符号执行对嵌入式汇编程序进行软件模型检查

• 发表时间: 2015
• 作者: 公下亮佑;山根 智
• 通讯作者: 山根 智