王 翀 吕荫润 陈 力 王秀利 王永吉

1(基础软件国家工程研究中心(中国科学院软件研究所) 北京 100190)2(中国科学院大学 北京 100049)3(计算机科学国家重点实验室(中国科学院软件研究所) 北京 100190)4 (中央财经大学信息学院 北京 100081)



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

王 翀1,2,3吕荫润1,2,3陈 力1,2,3王秀利4王永吉1,3

1(基础软件国家工程研究中心(中国科学院软件研究所) 北京 100190)2(中国科学院大学 北京 100049)3(计算机科学国家重点实验室(中国科学院软件研究所) 北京 100190)4(中央财经大学信息学院 北京 100081)

(wangchong@nfs.iscas.ac.cn)

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

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

近年来，随着可满足性模理论(satisfiability modulo theories, SMT)的不断进步以及互联网、云计算等新兴技术的不断发展，SMT被广泛地应用于各个领域，例如云……