SMT求解技术的发展及最新应用研究综述

摘要：

可满足性模理论(satisfiability modulo theories, SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.

关键词：可满足性模理论、SMT求解器、SMT求解算法、测试用例自动生成、程序缺陷检测、云计算

所属期刊栏目：54

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金项目61170072,61303057;中国科学院、国家外国专家局创新团队国际合作伙伴计划 This work was supported by the National Natural Science Foundation of China61170072,61303057;the CAS/SAFEA International Partnership Program for Creative Research Teams

在线出版日期：2017-08-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共21页

页码：1405-1425