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

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 technologies have to resort to many kinds of decision procedures and constraint solving algorithms. However, most traditional verification methods adopt one single constraint solving algorithm to do reasoning, which potentially restricts the scope of their applications. With the advance of safety-critical systems, this project mainly studies several decision procedures, constraint solving procedures and the combination problem of them, thus enlarging the scope of solvable constraints. Meanwhile it applies the above results to the verification fields of computer software programs, for the purpose of serving as a solid theoretical basis of trustworthy softwares. Besides, our preliminary result indicates that the combination of constraint solving procedures is an effective approach to reducing the computational complexity. Hence it gives rise to the prosiming “1+1>2” outcome. On the basis of it, this project also plans to devise efficient specialized verification tools for international and domestic communications.

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

现今信息技术已经渗透到日常生活的方方面面。如何提高信息计算系统的可靠性是一个不可回避的问题。为了追求绝对正确性，相关的验证离不开判定过程、约束求解方法。本项目首先重点研究各种复杂约束的求解算法，如 (i) 一类带有指数函数的公式的量词消去和 (ii) 将多项式次数从正整数推广到实代数数的广义多项式的正根隔离；其次，将它们有机地结合起来，并服务于计算系统的验证领域，如 (i) 可解动力系统的轨迹问题和 (ii) 马尔科夫报酬模型上的概率计算问题，都取得了良好的结果。在该项目支持下，我们发表了6篇高质量学术论文，其中：2篇发表在J. Symb. Comput.、2篇发表在Theoret. Comput. Sci.、1篇为ISSAC-2016，均第一标注本项目，圆满完成原定研究目标；我们还培养在读研究生4名（1名转博、在读3名）。根据国际上的最新热点，建议后续工作可由从确定性的计算模型转向概率性的计算模型，以期取得丰硕成果。