组合约束求解过程及其在程序验证中的应用

项目名称： 组合约束求解过程及其在程序验证中的应用

项目编号： No.11401218

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

立项/批准年度： 2014

项目学科： 数理科学和化学

项目作者： 徐鸣

作者单位： 华东师范大学

项目金额： 22万元

中文摘要： 现今信息技术已经渗透到日常生活的方方面面。如何提高信息计算系统的可靠性是一个不可回避的问题。为了追求绝对正确性这一目标，相关的验证与检测技术离不开各种判定过程、约束求解的理论方法。而传统的验证技术运用单一的约束求解算法进行推理，从一定程度上束缚了验证技术的应用范围。在安全攸关系统迅猛发展的时代背景下，本项目拟重点研究多种判定过程、约束求解算法和它们之间的组合问题，扩大可解约束的范围；成果也将同时应用于计算机软件程序的验证问题中，为可信软件提供扎实的理论基础。此外，通过预研的结果，组合约束求解还是降低计算复杂性的有效途径之一，有望达到“1+1>2”的良好效果。因此，本项目还计划研制相应的高效验证工具包，供国内外同行借鉴。

中文关键词： 符号计算；判定过程；约束求解；程序验证；安全攸关系统

英文摘要： Nowadays information technologies have a very deep impact on all aspects of our daily life. How to improve the reliability of information computing systems is a neglectable problem. To pursue the absolute correctness, related verification and testing tech

英文关键词： symbolic computation；decision procedure；constraint-solving；program verification；safety-critical system