项目名称: 面向数值程序安全性与鲁棒性的抽象解释技术

项目编号: No.61202120

项目类型: 青年科学基金项目

立项/批准年度: 2013

项目学科: 计算机科学学科

项目作者: 陈立前

作者单位: 中国人民解放军国防科学技术大学

项目金额: 26万元

中文摘要: 计算机软件尤其是嵌入式软件的设计与运行,与系统及环境的数学与物理模型密不可分,往往会涉及大量数值运算。计算机软件的许多可信性质和程序缺陷与程序中的数值性质密切相关。因此,研究数值程序安全性与鲁棒性的分析方法,对提高软件的可信性具有重要意义。本项目针对计算机中数值程序的特点,即数值数据类型值表示范围的有限性、浮点运算的不精确性、输入数据伴随的非确定性等特点,面向数值程序的安全性与鲁棒性,以抽象解释为理论支撑,开展相关静态分析技术研究。拟突破数值不变式生成、数值程序的安全性与鲁棒性分析等关键技术,力求在新型数值抽象域设计、浮点程序分析、命令式程序鲁棒性分析等关键科学问题的研究中获得进展和突破,设计并实现相应的数值程序分析工具原型,针对航空航天等领域典型嵌入式软件的数值相关性质进行示范应用。本项目将形成面向数值程序的静态分析方法、技术和工具,对计算机软件的可信保障具有重要实际应用价值。

中文关键词: 抽象解释;静态分析;数值程序;安全性;鲁棒性

英文摘要: Computer software especially embedded software has a tighten relation with the mathematical and physical model of the system and the environment, and thus often involves a lot of numeric computation. Hence, a variety of dependability properties and software defects are closely related to the numeric properties of programs. This project addresses the safety and robustness issues of numeric programs due to the finite representability of numeric data types, inexactness of floating point computation, and intrinsic uncertainty over input data. The main goal of this project is to develop new methods and tools at the source code level that fit for analyzing the safety and robustness of numeric programs, by exploiting the abstract interpretation theory. This project will explore and strengthen some core techniques, such as numeric invariant generation, safety analysis and robustness analysis of numeric programs, to target several scientific issues including the design of new numeric abstract domains, analysis of floating point programs, robustness analysis of imperative programs, etc. On this basis, this project plans to develop a prototype of static analyzer for numeric programs and apply it to analyze certain numeric related properties of domain-specific software, such as avionics and space embedded software. The proj

英文关键词: abstract interpretation;static analysis;numeric programs;safety;robustness

成为VIP会员查看完整内容
0

相关内容

深度学习模型鲁棒性研究综述
专知会员服务
88+阅读 · 2022年1月23日
专知会员服务
21+阅读 · 2021年10月8日
【干货书】Python科学编程,451页pdf
专知会员服务
125+阅读 · 2021年6月27日
【干货书】面向计算科学和工程的Python导论,167页pdf
专知会员服务
41+阅读 · 2021年4月7日
专知会员服务
87+阅读 · 2021年1月17日
专知会员服务
188+阅读 · 2020年10月14日
【干货书】图形学基础,427页pdf
专知会员服务
143+阅读 · 2020年7月12日
【干货书】数值计算C编程,319页pdf,Numerical C
专知会员服务
65+阅读 · 2020年4月7日
「深度学习模型鲁棒性」最新2022综述
专知
7+阅读 · 2022年1月23日
【开放电子书】概率编程导论,301页pdf
专知
4+阅读 · 2021年10月21日
智能合约的形式化验证方法研究综述
专知
13+阅读 · 2021年5月8日
【CVPR2021】现实世界域泛化的自适应方法
专知
5+阅读 · 2021年3月31日
【干货书】掌握Python算法,337页pdf
专知
1+阅读 · 2021年3月20日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2022年4月18日
小贴士
相关VIP内容
深度学习模型鲁棒性研究综述
专知会员服务
88+阅读 · 2022年1月23日
专知会员服务
21+阅读 · 2021年10月8日
【干货书】Python科学编程,451页pdf
专知会员服务
125+阅读 · 2021年6月27日
【干货书】面向计算科学和工程的Python导论,167页pdf
专知会员服务
41+阅读 · 2021年4月7日
专知会员服务
87+阅读 · 2021年1月17日
专知会员服务
188+阅读 · 2020年10月14日
【干货书】图形学基础,427页pdf
专知会员服务
143+阅读 · 2020年7月12日
【干货书】数值计算C编程,319页pdf,Numerical C
专知会员服务
65+阅读 · 2020年4月7日
相关基金
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2009年12月31日
微信扫码咨询专知VIP会员