程序和混成系统验证中的非线性问题研究

Program and hybrid system verification is an important assisting method to guarantee reliability and effectiveness for programs and hybrid systems. The research on program and hybrid system verification is a hot issue in both academia and industry all the times, and is also an important research field crossing the computer science and mathematics. In program and hybrid system verification, many problems can be transformed into constraints solving problem or deciding problem in nonlinear theories. But the results about nonlinear constraints solving and deciding are rarely, and most of the corresponding methods are usually low efficiency. This project start with the technical requirements of program verification, and centers on two main problems about nonlinear theories. First, we study the solving and deciding of nonlinear formulas, which include efficient solving methods for nonlinear formulas, the decision methods for satisfiability of non-polynomial formulas and nonlinear Craig interpolant generation. Second, we use the above methods to deal with program verification and hybrid system verification, which include using the methods of constraint solving and Craig interpolant generation to deal with program verification, using the methods of constraint solving and satisfiability to deal with hybrid system verification. This project intends to use symbolic-numerical computation as the dominant thought. We believe we would make progress in the research of the methods of efficient solving and deciding, and apply them to program verification and hybrid system verification.

程序和混成系统验证是保障程序和混成系统可靠性和有效性的重要手段。关于程序和混成系统验证的研究一直是学术界和工业界关注的热点，也是计算机科学与数学交叉的重要研究领域。其中很多问题都可以转化成非线性约束求解或判定问题。但是关于非线性约束求解和判定问题的结果却比较少，也十分低效。本项目从程序验证的理论和技术需求出发，围绕着非线性理论拟开展如下两个方面研究：一，非线性公式求解和判定。包括非线性约束的高效求解、非多项式理论性判定以及非线性Craig插值的生成；二，程序验证和混成系统验证。利用上述提出的方法解决相应的程序验证和混成系统验证问题，包括将非线性约束求解算法和非线性Craig插值生成方法应用于程序验证，将非线性公式约束求解算法和非多项式理论的判定方法应用于混成系统验证。本项目拟利用符合数值混合计算为主导思想，可望在非线性理论相关的高效求解和判定方法上有所突破，并应用到程序和混成系统验证上。

程序验证和混成系统验证是保障程序和混成系统可信性的重要手段。关于程序验证和混成系统验证的研究一直是学术界和工业界关注的热点，也是计算机科学与数学交叉的重要研究领域。在程序验证和混成系统验证中，很多的验证问题都可以转化成非线性理论的判定问题或者约束求解问题。本项目从程序验证和混成系统验证中涉及的非线性理论问题出发，研究非线性理论的判定和约束求解问题，并将相关方法应用于程序验证和混成系统验证。在本项目的支持下获得如下重要成果，1. 提出了一种高效的非线性约束求解算法，在理论上构造了非线性约束的等价性，具有很强的理论意义；2. 提出了一种非线性Craig插值生成算法和非线性循环不变式生成算法，为程序验证中的非线性问题提供技术支持，在程序验证上基于一定的应用价值；3. 提出了一种时延混成系统的安全控制器合成方法，为控制器系统提供了控制器合成技术支持，在控制器合成上具有很好的应用意义。项目达到了预期的研究目标，培养/毕业博士研究生2名，硕士研究生6名；在国际顶级/重要学术会议CAV2020、AAAI2021、IJCAI2022、HSCC2021、KDD2021、以及国内权威期刊中国科学-数学，计算机应用研究上发表高水平学术研究论文7篇，其中CCF推荐A类论文4篇、B类论文1篇、中文核心期刊1篇、CCF推荐C类中文期刊1篇。

内容获取失败，请点击重试