约束求解与定理证明专题前言  

作　　者：蔡少伟 陈振邦[2] 王戟[2] 詹博华 赵永望 

机构地区：[1]中国科学院软件研究所,北京100190 [2]国防科技大学计算机学院,湖南长沙410073 [3]浙江大学计算机科学与技术学院,浙江杭州310007

出　　处：《软件学报》2023年第8期3465-3466,共2页Journal of Software

摘　　要：随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求解和定理证明是形式化方法中的两大关键技术.在约束求解方面,SAT和SMT求解器已经在学术界和工业界得到了广泛应用,比如SAT求解器用于EDA领域的等价性验证,SMT求解器用于程序验证和白盒模糊测试等.交互式定理证明通过人和计算机之间的交互完成证明,能够验证非常复杂的系统和性质,例如编译器和操作系统的正确性验证.约束求解与定理证明专题关注约束求解和定理证明的理论、技术、工具与应用,包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用.

关 键 词：形式化方法 定理证明 约束求解 符号执行 计算机系统 模糊测试 模型检测 系统安全 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]