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

发布时间：2018-04-03 00:38

本文选题：可满足性模理论　切入点：SMT求解器　出处：《计算机研究与发展》2017年07期

【摘要】：可满足性模理论(satisfiability modulo theories,SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.
[Abstract]:Satisfiability modulo the SMTs is the background theory of determining the satisfiability problem of the first-order logic formula under combinatorial background theory, which enables it to describe all kinds of problems in practical fields.Combined with an efficient satisfiability determination algorithm, SMT has outstanding advantages in some new research fields, such as automatic generation of test cases, program defect detection and RTL register transfer level verification, program analysis and verification, optimization of linear logic constraint formula, and so on.At first, the basic problem of SMT problem and its judging algorithm are introduced. Secondly, the SMT problem is summarized, and the mainstream SMT solver, including Z3Yices2CVC4, is analyzed, and the practical application of SMT solution technology in typical field is emphasized.At last, the prospect of the future development of SMT is prospected, with the purpose of trying to promote the development of SMT, and to provide useful reference for the relevant personnel in this field.
【作者单位】：基础软件国家工程研究中心(中国科学院软件研究所);中国科学院大学;计算机科学国家重点实验室(中国科学院软件研究所);中央财经大学信息学院;
【基金】：国家自然科学基金项目(61170072,61303057) 中国科学院、国家外国专家局创新团队国际合作伙伴计划~~
【分类号】：TP301.6;TP311.53

【参考文献】