SMT求解器技术对比分析及其能力扩展研究

国防科学技术大学硕士学位论文SMT求解器技术对比分析及其能力扩展研究姓名：李婧申请学位级别：硕士专业：计算机科学与技术指导教师：王戟2010-11国防科学技术大学研究生院硕士学位论文第i页摘要形式化方法是一种有效的计算机软、硬件系统可信性验证手段。其主要技术包括模型检验，定理证明，等价性检验以及语言包含等。许多形式化验证问题昀终都归结于布尔可满足问题(SAT)，它用来判断命题逻辑公式是否为可满足的。SAT是第一个被证明的NP完全问题。与SAT相比，SMT问题具有表达能力更强、抽象层次更高的优点，因而，迅速成为了形式化验证中的重要问题。而本文重点关注两个问题：目前SMT求解器能力以及如何扩展SMT求解器能力。SMT问题属于一阶逻辑范畴，SMT求解器可判定的理论域包括：等式与未解释函数、线性算术、位向量以及量化公式等。而多种理论组合是适应当今工业应用日益复杂、多元化需求的，因此对该领域的判定技术的研究具有重大实际意义。本文对比分析了该技术的主要方法：Nelson-Oppen方法，DelayedTheoryCombination方法，Ackerman方法。另外，分析了主流求解器的关于该技术采用的昀新策略。本文面向工业应用构建测评框架，对比评测5个当前主流并可用的支持理论组合判定技术的SMT求解器。从实验结果中看出Z3所采用的基于模型的DTC方法使其整体性能昀佳，并且在各应用领域中Z3求解能力昀强，特别是量化问题领域。并非所有的理论域SMT求解器对其都具有完全判定方法，仍存在无法判定的SMT问题，特别是在量化领域。文中给出一类目前SMT求解器无法判定的量化SMT公式一般形式，并由此构造一个自动机的符号化表示，文中证明了该过程转换的正确性。昀终结合SMT公式解析模块和自动机语言判空技术，实现了一个完整的量化SMT公式判定过程。通过例子测试说明该方法的可行性并扩充了SMT求解器能力，是兼具理论价值和实际意义的。关键词：SMT，理论组合技术，量化SMT公式，自动机符号化表示，ω-自动机判空问题国防科学技术大学研究生院硕士学位论文第ii页ABSTRACTFormalmethodhasbeenproventobeaneffectivetechniqueinverifyingthetrustnessofsoftwareandhardwaresystems,anditincludesseveralapplicablemethodssuchasmodelchecking,theoryproving,equivalencecheckingaswellaslanguagecontainment.ManyoftheseformalmethodscanbetranslatedtoBoolean/PropositionalSatisfiabilityProblems(SAT),whichisusedtodecidewhetheraformulaaccordingtopropositionallogicissatisfied.SATiswell-knownasthefirstprovedNP-Completeproblem.ComparedwithSAT,SatisfiableModuleTheories(SMT)problemsaremoreexpressiveandabstractive,thusSMTbecomescriticalproblemsinverificationfield.Thisthesismainlyfocusesontwothings,oneistomakesureofthestate-of-the-artabilitiesofSMTsolvers,andtheotheristofindawaytoenlargeandcomplementthecapabilitiesofSMTsolvers.SMTproblembelongstofirst-orderlogicanditsdecidabletheoriesrangesoverfieldsasequalitiesanduninterpretedfunctions,lineararithmetic,bitvectorsaswellasquantifiedproblems.However,combinationofmutipletheoriesisconsideredtobewithgreatapplicablevaluesduetothedemandsofthepresentlycomplexandmulti-eraindustrialapplications.Thisarticlecomparativelyanalyzesthreeoftheorycombinationtechniques:Nelson-Oppen,DelayedTheoryCombinationandAckermannmethods.Besides,wepresentthenewesttechniquesforSMTsolversindealingwiththoerycombination,andthenacapabilitiesenvaluationplatformtotallyorientedtoreal-worldapplicationsforSMTsolversisgiven,wecomparativelytestingthelatestandusableverisionsoffiveSMTsolvers.Throughtheresults,wecanfindoutthatZ3beatsothersforthewholeperformancewiththerefinedDTCapproachbasedonmodel,especiallyindealingwithquatifiedformulas.NotallthetheorydomainsSMTsolvershavegotacompletedecidablemethod;therearestillsomeunsolvableSMTproblems,especiallythequantifiedproblems.ThisarticleshowsageneralizedformulapatternwhichSMTsloverscannotsolveatpresent.Anewmethodforsolvingthisformulapatternisproposed,weconstructasymbolicformofautomata,andthecorrectnessofthistranslatingprocesshasbeenprovedinthisarticle.Finally,werealizeacompletedecisionprocedureforquantifiedSMTformula,whichcombinesourtranslatingprogramwiththeinputparsermoduleandlanguagedecisiontechniqueofautomata.Resultsproveournewmethodisfeasiblible;besides,itstrengthensthecapabilityofSMTsolversandmakescontributionsbothtotheoreticlemeaningsandapplicatiblevalues.KeyWords：SMT,TheoryCombination,QuantifiedSMTFormula,SymbolicExpressionofAutomata,EmptynessProblemofω-Automata国防科学技术大学研究生院硕士学位论文第III页表目录表1.1SMT求解器总表...............................................................................................6表2.2ω-(字)自动机接收条件(不含Finite)的布尔编码...........................................16 表3.1SMT-COMP’08各求解器理论组合判定执行结果.......................................25 表3.2SMT-COMP’09各求解器理论组合判定执行结果.......................................25 表3.3SMT求解器理论组合判定方法.....................................................................26 表3.4按理论组合分类的实验结果统计表..............................................................27 表3.5按工业应用分类的实验结果统计表..............................................................29 表4.1运算符号表......................................................................................................33国防科学技术大学研究生院硕士学位论文第IV页图目录图1.1验证方法与验证引擎........................................................................................2 图1.2基于DPLL算法的SAT求解器.......................................................................3 图2.1自动机的一次运行示例..................................................................................15 图2.2各类自动机表达能力之间的关系..................................................................17 图3.1NO方法传递接口等式...................................................................................20 图3.2改进NO方法传递接口等式实现非凸理论判定..........................................21 图3.3NO方法框架图(左)、DTC方法框架图(右).................................................22 图4.1迁移系统的符号化表示示意图......................................................................35 图4.2为例1构造的自动机M1(F)及其符号化表示.............................................37 图5.1实验基本框架图..............................................................................................42 图5.2例1smtlib格式源文件：testcase1.smt...........................................................44 图5.3CVC3对testcase1