中文摘要：

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