王 翀 呂蔭潤(rùn) 陳 力 王秀利 王永吉

1(基礎(chǔ)軟件國(guó)家工程研究中心(中國(guó)科學(xué)院軟件研究所) 北京 100190)2(中國(guó)科學(xué)院大學(xué) 北京 100049)3(計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室(中國(guó)科學(xué)院軟件研究所) 北京 100190)4 (中央財(cái)經(jīng)大學(xué)信息學(xué)院 北京 100081)

?

SMT求解技術(shù)的發(fā)展及最新應(yīng)用研究綜述

王 翀1,2,3呂蔭潤(rùn)1,2,3陳 力1,2,3王秀利4王永吉1,3

1(基礎(chǔ)軟件國(guó)家工程研究中心(中國(guó)科學(xué)院軟件研究所) 北京 100190)2(中國(guó)科學(xué)院大學(xué) 北京 100049)3(計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室(中國(guó)科學(xué)院軟件研究所) 北京 100190)4(中央財(cái)經(jīng)大學(xué)信息學(xué)院 北京 100081)

(wangchong@nfs.iscas.ac.cn)

可滿(mǎn)足性模理論(satisfiability modulo theories, SMT)是判定一階邏輯公式在組合背景理論下的可滿(mǎn)足性問(wèn)題.SMT的背景理論使其能很好地描述實(shí)際領(lǐng)域中的各種問(wèn)題,結(jié)合高效的可滿(mǎn)足性判定算法，SMT在測(cè)試用例自動(dòng)生成、程序缺陷檢測(cè)、RTL(register transfer level)驗(yàn)證、程序分析與驗(yàn)證、線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解等一些最新研究領(lǐng)域中有著突出的優(yōu)勢(shì).首先闡述SMT問(wèn)題的基礎(chǔ)SAT(satisfiability)問(wèn)題及判定算法；其次對(duì)SMT問(wèn)題、判定算法進(jìn)行了總結(jié),分析了主流的SMT求解器,包括Z3，Yices2，CVC4等；然后著重介紹了SMT求解技術(shù)在典型領(lǐng)域中的實(shí)際應(yīng)用,對(duì)目前的研究熱點(diǎn)進(jìn)行了闡述；最后對(duì)SMT未來(lái)的發(fā)展前景進(jìn)行了展望,目的是試圖推動(dòng)SMT的發(fā)展,為此領(lǐng)域的相關(guān)人員提供有益的參考.

可滿(mǎn)足性模理論；SMT求解器；SMT求解算法；測(cè)試用例自動(dòng)生成；程序缺陷檢測(cè)；云計(jì)算

近年來(lái)，隨著可滿(mǎn)足性模理論(satisfiability modulo theories, SMT)的不斷進(jìn)步以及互聯(lián)網(wǎng)、云計(jì)算等新興技術(shù)的不斷發(fā)展，SMT被廣泛地應(yīng)用于各個(gè)領(lǐng)域，例如云計(jì)算與云存儲(chǔ)[1-2]、訪(fǎng)問(wèn)控制[3-4]、多核問(wèn)題[5-6]、程序缺陷檢測(cè)驗(yàn)證[7]、有界模型檢測(cè)[8-9]、RTL驗(yàn)證[10]、優(yōu)化問(wèn)題求解[11-12]、靜態(tài)分析[13-14]、程序驗(yàn)證[15-16]等等.這些領(lǐng)域中待解決的實(shí)際問(wèn)題都可以建模為約束可滿(mǎn)足問(wèn)題，SMT在這類(lèi)問(wèn)題的表述和求解上有突出優(yōu)勢(shì).

計(jì)算機(jī)科學(xué)和數(shù)理邏輯中的SAT(satisfiability)問(wèn)題是命題邏輯公式的可滿(mǎn)足性問(wèn)題.1971年，Cook[17]證明了SAT問(wèn)題是非確定性多項(xiàng)式完全(non-deterministic polynomial-time complete, NPC)問(wèn)題，SAT問(wèn)題也是第1個(gè)被證明了的NPC問(wèn)題.

起初，人們注重研究SAT在硬件測(cè)試、電路驗(yàn)證等領(lǐng)域中的應(yīng)用，SAT求解技術(shù)的發(fā)展對(duì)自動(dòng)電子設(shè)計(jì)(electronic design automation， EDA)領(lǐng)域中相關(guān)問(wèn)題的研究起到了重要作用.隨后SAT被廣泛地應(yīng)用于各個(gè)新興領(lǐng)域，例如靜態(tài)程序分析[18-20]、測(cè)試用例生成[21-23]等.SAT只面向命題邏輯公式，表達(dá)能力有較高的局限性，因此將實(shí)際問(wèn)題轉(zhuǎn)化為SAT問(wèn)題時(shí)會(huì)丟失很多高層級(jí)(high-level)信息.例如在RTL驗(yàn)證中，SAT使用位向量描述原問(wèn)題會(huì)導(dǎo)致大量邏輯信息的丟失，降低了結(jié)果的準(zhǔn)確性.

由于上述缺點(diǎn)，人們將SAT擴(kuò)展為SMT.SMT面向一階邏輯公式，在命題邏輯的基礎(chǔ)上補(bǔ)充了量詞和項(xiàng)，具有更強(qiáng)的表達(dá)能力.SMT融合了多種背景理論，公式中的命題變量可以是理論公式，能夠直接描述問(wèn)題中的高層級(jí)信息.例如SMT的數(shù)組理論能直接描述數(shù)組定義和相關(guān)操作.實(shí)際應(yīng)用中的理論不僅限于單一理論，通常是多個(gè)理論的組合.比如線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解[11]需要線(xiàn)性實(shí)數(shù)理論和未解釋函數(shù)理論等理論的支持；有界模型檢[7]測(cè)需要數(shù)組理論、未解釋函數(shù)理論和位向量等理論的支持；驗(yàn)證條件分析和定理證明[24]需要數(shù)組理論、未解釋函數(shù)和線(xiàn)性整數(shù)算術(shù)理論等理論的支持.

SMT求解技術(shù)的具體實(shí)現(xiàn)被稱(chēng)為SMT求解器(SMT solvers).最初的SMT求解器[25-27]是研究人員為形式化方法設(shè)計(jì)的判定算法，直到1990年，可以處理大規(guī)模實(shí)際問(wèn)題的SMT求解器[28-32]成為了新的研究熱點(diǎn).近年來(lái)，SMT求解技術(shù)的發(fā)展情況如下：

1) 核心算法、數(shù)據(jù)結(jié)構(gòu)以及現(xiàn)代微處理器的發(fā)展使得SAT求解器[33]可以處理含有數(shù)萬(wàn)變量的公式，以SAT求解器為基礎(chǔ)的SMT求解技術(shù)隨之提升；

2) SMT求解技術(shù)的廣泛應(yīng)用前景使得各個(gè)科研機(jī)構(gòu)積極開(kāi)發(fā)SMT求解器；

3) 年度SAT競(jìng)賽*http:www.satcompetition.org和SMT競(jìng)賽*http:www.smtcomp.org推動(dòng)了SMT求解技術(shù)的發(fā)展；

4) SMT-LIB(satisfiability modulo theories library)標(biāo)準(zhǔn)的出現(xiàn)使得SMT求解器開(kāi)發(fā)變得更加容易.人們研發(fā)了很多SMT求解器，比較成熟的有Z3[34]，CVC4[35]，Yices2[36]，MathSAT4[37]，Boolector[38].SMT求解器也被集成到一些大型工具中，例如微軟開(kāi)發(fā)的PEX[39]工具，其主要功能是研究和分析托管代碼.Henzinger等人[40]開(kāi)發(fā)的BLAST工具是一個(gè)C語(yǔ)言軟件模型檢測(cè)工具，其實(shí)現(xiàn)主要依賴(lài)于謂詞抽象和插值技術(shù).

國(guó)內(nèi)外研究人員對(duì)SMT進(jìn)行了相關(guān)的研究和總結(jié).王建新等人[41]給出了SAT問(wèn)題定義和分類(lèi)的綜述，對(duì)各類(lèi)衍生SAT問(wèn)題進(jìn)行了闡述和舉例說(shuō)明;Sheini等人[42]闡述了SAT和SMT的基本概念，介紹了基于SAT技術(shù)的SMT問(wèn)題及求解方法等內(nèi)容;Moura等人[43]對(duì)SMT求解技術(shù)和背景理論進(jìn)行了詳細(xì)地介紹;金繼偉等人[44]對(duì)SMT求解技術(shù)進(jìn)行了簡(jiǎn)述，包括SMT的部分背景理論、SMT判定算法及優(yōu)化，重點(diǎn)介紹了SMT的基礎(chǔ)知識(shí)及SMT求解器的基本情況.

SMT的實(shí)際應(yīng)用是目前的研究熱點(diǎn)，但是缺乏對(duì)SMT最新應(yīng)用及最新進(jìn)展進(jìn)行綜述的文章，也缺乏對(duì)SMT競(jìng)賽進(jìn)行歸納和分析的文章.本文試圖全面地介紹SMT在工業(yè)界和學(xué)術(shù)界中的最新主流應(yīng)用，并根據(jù)目前SMT領(lǐng)域中公認(rèn)度最高的SMT-COMP(international satisfiability modulo theories competition)，比較主流SMT求解器的綜合性能及支持背景理論的數(shù)量.為了文章的完整性以及易于后續(xù)研究人員理解，本文從SMT的起源，即SAT問(wèn)題開(kāi)始，簡(jiǎn)潔而又力求全面地介紹SMT的發(fā)展過(guò)程，詳細(xì)闡述SAT，SMT判定算法及理論組合判定算法，分析算法的原理及實(shí)現(xiàn)過(guò)程，希望對(duì)程序分析與驗(yàn)證、軟件缺陷檢測(cè)等領(lǐng)域的研究提供支持.

1 SAT問(wèn)題及判定算法

1.1 SAT問(wèn)題

SAT問(wèn)題是命題邏輯公式(propositional logical formula)的可滿(mǎn)足性判定問(wèn)題，下面先介紹有關(guān)命題邏輯的一些必要概念.命題邏輯中的邏輯運(yùn)算符號(hào)(又稱(chēng)二元連接符)是指定義在布爾集合上的邏輯運(yùn)算，包括∧(與)，∨(或)，(非)，→(蘊(yùn)含)，?(等價(jià))，⊕(異或).命題變?cè)娜≈禐檎婊驗(yàn)榧?，在取值意義上等價(jià)為布爾變量.命題邏輯公式的形成規(guī)則為

1) 命題邏輯公式f(或SAT公式f)可以是單獨(dú)的命題變?cè)?，也稱(chēng)為原子公式;

2) 如果f是命題邏輯公式，那么f也是命題邏輯公式;

3) 如果f1和f2是命題邏輯公式，那么f1⊥f2也是命題邏輯公式，其中⊥∈{∧，∨，，→，?，⊕}.原子公式f與其否定命題f統(tǒng)稱(chēng)為文字，而1個(gè)子句由若干個(gè)文字析取而成.

基于命題邏輯，SAT問(wèn)題可以進(jìn)一步被描述為：給定1個(gè)命題邏輯公式f，公式f由子句集S組成，其中S由1組布爾變量V組成，判定是否存在1組對(duì)于f的賦值使得f中所有子句取值為真，如果存在，則稱(chēng)公式f可滿(mǎn)足；否則，f不可滿(mǎn)足.判定f是否可滿(mǎn)足是SAT問(wèn)題的核心.

隨著SAT求解技術(shù)不斷的發(fā)展，SAT問(wèn)題的衍生問(wèn)題也成為了研究熱點(diǎn)，例如帶權(quán)可滿(mǎn)足性問(wèn)題(weighted satisfiability)[45]、參數(shù)化帶權(quán)可滿(mǎn)足性問(wèn)題(3-CNFSAT，q-CNFSAT)[45]、最大可滿(mǎn)足性問(wèn)題(maximum satisfiability)[46]、帶權(quán)最大可滿(mǎn)足性問(wèn)題(weighted MAX-SAT)[47]、參數(shù)化MAXSAT問(wèn)題[48]、參數(shù)化Almost2-SAT問(wèn)題(parameterized2-ASAT)[48]等.

1.2 SAT問(wèn)題判定算法

SAT問(wèn)題判定算法可以分為2類(lèi)：局部搜索算法和完備算法(回溯搜索算法).局部搜索算法基于隨機(jī)搜索策略，對(duì)于任意給定的問(wèn)題，它不一定能判斷該問(wèn)題是否可解；而完備算法基于窮舉和回溯的思想，可以判斷給定的問(wèn)題是否可滿(mǎn)足，對(duì)于無(wú)解問(wèn)題擁可給出無(wú)解的證明.判定SAT問(wèn)題時(shí)，需要確定給出的問(wèn)題是否可滿(mǎn)足，因此完備算法是研究的重點(diǎn).

基于搜索回溯的SAT問(wèn)題判定算法由Davis和Putnam在1960年提出，稱(chēng)為DP(Davis-Putnam)算法[49].該算法不適用于大規(guī)模命題公式的可滿(mǎn)足性問(wèn)題判定，因此Davis，Putnam，Logemann，Loveland對(duì)DP算法進(jìn)行了改進(jìn)，改進(jìn)后的算法稱(chēng)為DPLL(Davis-Putnam-Logemann-Loveland)算法[50].

DPLL算法包括的主要操作為推理(unit-propagation)、純文字(pure-literal)、決策(decide)、不可滿(mǎn)足(fail)和回溯(backtrack).

unit-propagation對(duì)于子句取值未定義并且只含1個(gè)取值未定義的變量，可以直接令該變量取值為真并加入到賦值中，并根據(jù)當(dāng)前賦值情況對(duì)搜索空間進(jìn)行裁剪.若文字l在賦值中被判定為真，則公式f中所有含有l(wèi)的子句都可以從搜索空間中刪除，含有l(wèi)的子句可以將l去掉.

pure-literal規(guī)則用于化簡(jiǎn)公式f中的變量，若f中僅存在l或l中的1種形式，則l的值可以立即被判定并從搜索空間中刪除包含l的子句.

decide通過(guò)一些策略來(lái)選取1個(gè)尚未賦值的變量，并將它的值指定為真或假.

fail用于檢測(cè)公式f在當(dāng)前搜索空間下的可滿(mǎn)足性以及是否存在沖突.

backtrack在fail檢測(cè)到公式f在當(dāng)前搜索空間不可滿(mǎn)足時(shí)進(jìn)行回溯，返回到上1層搜索空間并通過(guò)decide重新尋找賦值變量.

DPLL算法的輸入是SAT公式f，輸出為真(true)或者假(false)，主要步驟如下：

1) 使用fail操作判斷f的可滿(mǎn)足性，如果不可滿(mǎn)足則返回false；

2) 使用decide操作對(duì)f中1個(gè)未賦值的變量進(jìn)行賦值；

3) 使用unit-propagation操作裁剪搜索空間；

4 )使用pure-literal規(guī)則化簡(jiǎn)f；

5) 使用fail判斷f的可滿(mǎn)足性，若f可滿(mǎn)足，則返回true；

6) 使用fail判斷f是否存在沖突，如果f不存在沖突，則返回步驟2，否則使用backtrack進(jìn)行回溯；

7) 如果回溯失敗，則返回false，否則執(zhí)行回溯并返回步驟2.

現(xiàn)代DPLL搜索算法均是在此基礎(chǔ)上進(jìn)行改進(jìn)的，典型的基于沖突檢測(cè)的子句學(xué)習(xí)求解算法CDCL(conflict-driven clause learning SAT solver, CDCL)描述如下所示：

算法1. CDCL求解算法.

CDCL(f,v)

UnitPropagation(f,v)

if (ConflictDetection()=Conflict)

returnunsatisfiable；

end if

DecisionLevel=0；

while (notAllVariableAssigned())

(x,v)=FindBranchingVariable(f,v)；

DecisionLevel=DecisionLevel+1；

UnitPropagation(f,v)；

if(ConflictDetection()=Conflict)

ConflictLevel=ConflictAnalysis(f,v)；

if(ConflictLevel<0)

returnunsatisfiable;

else

Backtrack(f,v,ConflictLevel)

dl=ConflictLevel；

end if

end if

end while

returnsatisfied.

CDCL算法與DPLL算法的最大區(qū)別在于每當(dāng)UnitPropagation執(zhí)行完成后，ConflictDetetction便會(huì)檢測(cè)是否存在沖突，若存在沖突，則調(diào)用ConflicAnalysis分析沖突產(chǎn)生的原因并進(jìn)行子句學(xué)習(xí)，以此確定回溯的層次.

現(xiàn)代SAT求解器采用了加速搜索的相關(guān)策略，例如啟發(fā)式變量決策提升了decide操作的效率，學(xué)習(xí)子句刪除減少了內(nèi)存的消耗和性能的損失，搜索重啟有利于對(duì)變量的決策順序進(jìn)行調(diào)整.研究人員也提出了一些改進(jìn)的求解算法，比如Prestwich[51]在2006年提出的RANGER算法結(jié)合了貪心隨機(jī)算法，求解速度比回溯算法快.Audemard等人[52]在2007年提出了GUNSAT算法，該算法的核心是局部搜索算法，可以求解不可滿(mǎn)足問(wèn)題.許道云等人[53]在2007年提出了帶文字改名策略的DPLL算法，使用文字改名規(guī)則、消解規(guī)則、子公式規(guī)則和重復(fù)規(guī)則完成不可滿(mǎn)足公式的反駁證明工作.

2 SMT問(wèn)題及判定算法

2.1 SMT問(wèn)題及背景理論

SMT問(wèn)題的基礎(chǔ)是一階邏輯公式，在命題邏輯的基礎(chǔ)上補(bǔ)充了項(xiàng)和量詞，公式中的函數(shù)和謂詞符號(hào)需要用對(duì)應(yīng)的背景理論解釋.通常情況下，SMT公式是無(wú)量詞(存在、任意)的一階邏輯公式(quantifier free formula)，判定公式可滿(mǎn)足性的問(wèn)題稱(chēng)為SMT問(wèn)題.

使用SMT描述實(shí)際問(wèn)題并將問(wèn)題等價(jià)的轉(zhuǎn)化為SMT公式時(shí)，需要將一些數(shù)學(xué)理論、數(shù)據(jù)結(jié)構(gòu)理論與公式相結(jié)合，這些理論稱(chēng)為SMT背景理論，可以增強(qiáng)SMT公式的表達(dá)能力.基于背景理論的SMT問(wèn)題可以進(jìn)一步被描述為：給定1個(gè)背景理論T和1個(gè)SMT公式F，F(xiàn)是T-可滿(mǎn)足的(T-satisfiable)[54]當(dāng)且僅當(dāng)存在1個(gè)賦值使得公式F和背景理論T同時(shí)滿(mǎn)足，即F∪{T}是可滿(mǎn)足的.

SMT-LIB[55]是公認(rèn)程度較高的SMT研究標(biāo)準(zhǔn)，主要包括：

1) 規(guī)定了SMT求解器標(biāo)準(zhǔn)輸入輸出的語(yǔ)言規(guī)范；

2) 建立了格式嚴(yán)格統(tǒng)一的背景理論知識(shí)測(cè)試集，用來(lái)評(píng)價(jià)和比較SMT求解器的求解能力；

3) 提出了SMT背景理論的規(guī)范，主要分為未解釋函數(shù)理論(quantifier free_uninterpreted function, QF_UF)、數(shù)組理論(quantifier free_arrays, QF_AQF_AX)、整數(shù)集實(shí)數(shù)集上的線(xiàn)性算數(shù)理論(quantifier free_linear integer arithmeticquantifier free_linear real arithmetic, QF_LIAQF_LRA)、整數(shù)集實(shí)數(shù)集上的非線(xiàn)性算數(shù)理論(quantifier free_non_linear integer arithmeticquantifier free_non_linear real arithmetic, QF_NIAQF_NRA)、整數(shù)差分邏輯理論(quantifier free-difference logic over the integers, QF_IDL)、實(shí)數(shù)差分邏輯理論(quantifier free_difference logic over the reals, QF_RDL)、位向量理論(QF_BV)等.

在目前的實(shí)際應(yīng)用中，主流SMT求解器支持并實(shí)現(xiàn)的主要理論有6個(gè):

規(guī)則1. 如果i=j，則有select(store(array,i,v),j)=v.

規(guī)則2. 如果i≠j，則有select(store(array,i,v),j)=select(a,j).

數(shù)組背景理論中的相等關(guān)系需要通過(guò)未解釋函數(shù)理論進(jìn)行定義，例如(array=array′∧i=j)被等價(jià)地定義為(select(array,i)=select(array′,j)).基于QF-UF可以對(duì)數(shù)組背景理論可以進(jìn)行如下擴(kuò)展：

規(guī)則3. 對(duì)于2個(gè)相等的數(shù)組array和array′，任意1個(gè)整數(shù)(并且是數(shù)組的下標(biāo))i使得等式select(array,i)=select(array′,i)成立.

規(guī)則4. 對(duì)于2個(gè)不相等的數(shù)組array和array′，存在1個(gè)整數(shù)(并且是數(shù)組的下標(biāo))i使得等式select(array,i)≠select(array′,i)成立.

2) QF_IDL和QF_RDL.這2種理論的公式通常表示為

x1-x2⊙J，

(1)

其中，x1和x2表示實(shí)數(shù)或者整數(shù)變量，⊙∈{=,≥,≤,≠}，J是1個(gè)常量.

3) QF_UF.此背景理論中主要包含沒(méi)有經(jīng)過(guò)解釋的函數(shù)符號(hào)，比如f(x,y)，g(h(z))等，每個(gè)函數(shù)符號(hào)都可以被賦予不同的含義.

4) QF_BV.此理論主要用于處理位向量相關(guān)操作，例如左移、右移等.

c1x1+c2x2+…+cixi+…+cnxn⊙J，

(2)

其中，c1,c2,…,cn為常系數(shù)，x1,x2,…,xn為整數(shù)變量(在理論QF_LIA中)或?qū)崝?shù)變量(在理論QF_LRA中)，⊙∈{=,≥,≤,≠}.

求解線(xiàn)性不等式集是QF_LIA或QF_LRA理論的1個(gè)主要應(yīng)用，比如F=x>3∧y<4，令x=6∧y=3可使F為真.

以上介紹了目前應(yīng)用較為廣泛的主流理論，SMT-LIB目前支持的理論及相互之間的關(guān)系如圖1所示.

一些主流SMT求解器(比如Z3，CVC3，Boolector)對(duì)線(xiàn)性、非線(xiàn)性、位向量等背景理論的描述為[7,55]

(3)

(4)

(5)

(6)

Extract(B,i,j)|SignExt(B,k)|ZeroExt(B,k)，

(7)

(8)

Fig. 1 SMT-LIB background theories and their relations with each other[55]圖1 SMT-LIB理論之間的關(guān)系[55]

其中，L代表布爾值表達(dá)式，由A和L組成，代表邏輯運(yùn)算符非.con是邏輯連接符，包括合取(∧)、析取(∨)、蘊(yùn)含(→)、等價(jià)(?)、異或(⊕).B代表由整數(shù)、實(shí)數(shù)、位向量構(gòu)成的項(xiàng)，～代表補(bǔ)運(yùn)算，Const表示常量，Id表示變量.ite(cb,t1,t2)表示if-then-else，如果布爾表達(dá)式cb的值為真，則執(zhí)行t1，否則執(zhí)行t2.Extract(B,i,j)表示抽取位向量B的第i到第j位，產(chǎn)生1個(gè)新的長(zhǎng)度為i-j+1的位向量.SignExt(B,k)表示用k個(gè)0擴(kuò)展位向量B，形成新的長(zhǎng)度增加了k位的帶符號(hào)位向量.ZeroExt(B,k)跟SignExt(B,k)操作類(lèi)似，區(qū)別在于ZeroExt(B,k)生成不帶符號(hào)的位向量.op代表操作符，包括與(&)、或(|)、四則運(yùn)算符(+，-，*，)、右移(?)、左移(?)、位向量的級(jí)聯(lián)(@).

2.2 組合背景理論求解方法

由實(shí)際應(yīng)用問(wèn)題等價(jià)轉(zhuǎn)化而成的SMT問(wèn)題通常包含多種理論，需要結(jié)合數(shù)組、整數(shù)線(xiàn)性算數(shù)、實(shí)數(shù)差分邏輯等多種背景理論才能解釋SMT公式F中每一項(xiàng)的含義，這種情況下單理論判定方法無(wú)法滿(mǎn)足判定需求，需要組合理論判定方法的支持，主要方法有：Nelson-Oppen(NO)方法[58]、Delayed Theory Combination(DTC)方法[59]和Ackerman方法[60].

Fig. 2 The difference between NO and DTC圖2 NO方法和DTC方法的區(qū)別

Nelson等人[58]于1979年提出的Nelson-Oppen方法是最為經(jīng)典的組合理論求解方法，其他方法都是以此為基礎(chǔ)改進(jìn)而成的.Nelson-Oppen方法的前提是各個(gè)背景理論符號(hào)集不相交且各理論之間相互獨(dú)立，每個(gè)背景理論Ti中的無(wú)量詞SMT公式都需要有1個(gè)可滿(mǎn)足賦值Mi(基于理論的模型).Nelson-Oppen方法首先在各個(gè)理論間傳遞含有共享變量的等式，稱(chēng)為接口等式(interface equation)，然后各個(gè)理論將此接口等式加入到自己的約束條件中并進(jìn)行可滿(mǎn)足性判定.如果出現(xiàn)不可滿(mǎn)足的理論，則此SMT公式是不可滿(mǎn)足的，否則重復(fù)上述步驟直至沒(méi)有新的接口等式可以傳遞.如果此時(shí)沒(méi)有不可滿(mǎn)足的理論，則此SMT公式是可滿(mǎn)足的.Nelson-Oppen方法的缺點(diǎn)是過(guò)于依賴(lài)于共享變量的傳遞，并且提取共享變量又需要求解器進(jìn)行純化操作，需要各個(gè)背景理論間相互傳遞接口等式.負(fù)責(zé)的算法框架使得Nelson-Oppen方法求解效率低下.

Delayed Theory Combination方法由Bozzano等人[59]提出，避免了各個(gè)背景理論間的接口等式傳遞步驟，將組合理論的可滿(mǎn)足性判定請(qǐng)求統(tǒng)一交給頂層求解器處理，簡(jiǎn)化了求解框架，求解效率好于Nelson-Oppen方法.Nelson-Oppen方法和Delayed Theory Combination方法的區(qū)別如圖2所示.

Ackerman方法是Nelson等人[60]基于Nelson-Oppen方法提出的改進(jìn)算法，主要用于求解含有未解釋函數(shù)理論的組合背景理論問(wèn)題，通常和DTC方法結(jié)合使用.但是此方法具有局限性，僅提升在未解釋函數(shù)理論下SMT的求解效率.

2.3 SMT問(wèn)題判定算法

2.3.1 求解SMT問(wèn)題的積極類(lèi)算法

積極類(lèi)算法直接將SMT公式轉(zhuǎn)化為可滿(mǎn)足性意義上等價(jià)的SAT公式[61]，然后利用SAT求解器進(jìn)行求解工作.這個(gè)方法的好處在于它可以充分利用高效的SAT求解器，不用針對(duì)SMT的復(fù)雜背景理論去開(kāi)發(fā)特定理論求解器，積極類(lèi)算法是早期求解SMT問(wèn)題的主要方法，主要包括Per-Constraint Encoding[62-63]方法和Small-Domain Instantiation[64-65]方法.

Per-Constraint Encoding方法是指：對(duì)于SMT公式F，如果F含有未解釋函數(shù)，則通過(guò)Goel等人[66]提出的方法將SMT公式F轉(zhuǎn)化為基于可滿(mǎn)足意義上等價(jià)的SAT公式，主要思想是將F中的所有形如ai=aj的項(xiàng)用1個(gè)新的變?cè)猙ij來(lái)表示，再用SAT求解器對(duì)公式F進(jìn)行求解.bij需要滿(mǎn)足傳遞性，即(bij∧bjk)→bik.

Small-Domain Instantiation方法是指：對(duì)于SMT公式F，如果F中的項(xiàng)只包含變?cè)?，則用布爾變量組成的位向量代替公式中的變?cè)?，將SMT公式轉(zhuǎn)化為基于可滿(mǎn)足性意義上等價(jià)的SAT公式，利用SAT求解器求解公式F的可滿(mǎn)足性，達(dá)到求解原SMT公式可滿(mǎn)足性的目的.如果公式F除了變?cè)膺€包含未解釋函數(shù)，則需要利用Ackerman方法將公式F轉(zhuǎn)化為只包含等式邏輯的公式，然后判定F的可滿(mǎn)足性.

積極類(lèi)算法的求解效率依賴(lài)于實(shí)際問(wèn)題建模為SAT問(wèn)題的效率和SAT求解器自身的效率.隨著實(shí)際應(yīng)用問(wèn)題規(guī)模的不斷增大，建模為SAT問(wèn)題后得到的SAT公式長(zhǎng)度呈現(xiàn)指數(shù)級(jí)增長(zhǎng)的趨勢(shì)，算法的時(shí)間開(kāi)銷(xiāo)難以接受.因此，這類(lèi)算法并不適用于求解工業(yè)界的大規(guī)模實(shí)際應(yīng)用問(wèn)題.

2.3.2 求解SMT問(wèn)題的惰性算法

惰性算法[29]是目前大多數(shù)SMT求解器采用的算法[67-69]，算法主要步驟如下：

1) 對(duì)SMT公式進(jìn)行預(yù)處理，把公式中的命題變量替換為布爾變量，再將SMT公式轉(zhuǎn)化為可滿(mǎn)足性意義上等價(jià)的SAT公式；

2) 檢查此SAT公式是否可滿(mǎn)足，如果不可滿(mǎn)足，那么SMT公式也不可滿(mǎn)足，算法結(jié)束；

3) 如果SAT公式可滿(mǎn)足，則結(jié)合SMT背景理論去判斷SMT公式的可滿(mǎn)足性，返回判斷結(jié)果，算法結(jié)束.

此算法的優(yōu)勢(shì)在于，若算法在步驟2中已判定SAT公式不可滿(mǎn)足，則無(wú)需進(jìn)行后續(xù)判定工作，提高了求解效率.惰性算法是SAT求解器與對(duì)應(yīng)的背景理論相結(jié)合的產(chǎn)物，典型的惰性算法是DPLL(T)[70-71]算法.

DPLL(T)算法偽代碼如下：

算法2. DPLL(T).

輸入：SMT公式F；

輸出：true(真)或者false(假).

預(yù)處理公式F得到F的SAT形式的公式f

if (f是不可滿(mǎn)足的)

return false;

else

for (每個(gè)f的模型M)

檢查M是否與背景理論一致;

if (存在一個(gè)與背景理論一致的模型M)

return true;

end if

end for

if (每一個(gè)模型M都與背景理論不一致)

return false;

end if

end if

DPLL(T)算法的基礎(chǔ)是通用求解架構(gòu)DPLL(X)，此架構(gòu)獨(dú)立于具體的背景理論，將X替換為某個(gè)具體的背景理論T即可成為針對(duì)此背景理論的具體求解算法.但是在求解過(guò)程中，背景理論求解器的參與程度較小，通過(guò)理論預(yù)處理、選擇分支、理論沖突分析、理論推導(dǎo)等技術(shù)可以提升背景理論求解器的參與程度，從而獲得更高的求解效率[67-68,71-72]，Sebastiani[73]使用優(yōu)化技術(shù)同樣達(dá)到了提高求解效率的目的.

一些研究人員注重于如何將SAT求解器與背景理論更好地結(jié)合以獲得更高的求解效率，并做了相關(guān)的研究[67,74-75].

3 SMT求解器及性能比較

隨著SMT背景理論的逐漸成熟以及SMT問(wèn)題判定算法的不斷發(fā)展，許多SMT求解器能夠滿(mǎn)足學(xué)術(shù)界的研究需求，一些成熟的SMT求解器也能處理大規(guī)模工業(yè)化的應(yīng)用問(wèn)題.目前主要的求解器有：Z3[34]，CVC3[57]，CVC4[35]，Boolector[38]，Yices2[36]，MathSAT[76]，Mathsat4[37]，Verifun[75]，Beaver[77]，TSAT[78]，Barcelogic[79]，VeriT[80]等.下面重點(diǎn)介紹4個(gè)有代表性的SMT求解器.

Z3以其優(yōu)秀的綜合求解能力被業(yè)界所認(rèn)可，是目前為止在擴(kuò)展性、表達(dá)能力以及求解效率等方面都較為出色的SMT求解器.Z3的求解框架集成了基于DPLL的SAT求解器，并支持未解釋函數(shù)、算術(shù)運(yùn)算、數(shù)組等背景理論，核心求解算法是DPLL(T)算法和DTC方法.許多工業(yè)界的項(xiàng)目都用到了Z3，例如Pex[39]，HAVOC[81]，Yogi[82]，SLAMSDV[83]，Vigilante[84]等.

CVC3和CVC4是紐約大學(xué)和愛(ài)荷華大學(xué)聯(lián)合開(kāi)發(fā)的SMT求解器，使用SAT求解器和理論求解器的Search Engine作為核心求解框架，支持支持多種理論的求解.與CVC3相比，CVC4能更好地支持SMT-LIB并且優(yōu)化了求解框架.

Yices2是SRI International計(jì)算機(jī)科學(xué)實(shí)驗(yàn)室開(kāi)發(fā)的SMT求解器，前身是Yices，支持?jǐn)?shù)組理論、線(xiàn)性算數(shù)運(yùn)算理論、位向量理論，核心求解算法是優(yōu)化后的同余閉包算法.在組合理論的求解方面，Yices使用位移等式改進(jìn)了傳統(tǒng)的Nelson-Oppen方法，并結(jié)合動(dòng)態(tài)Ackerman方法進(jìn)行求解.在實(shí)際應(yīng)用領(lǐng)域，Yices作為定理證明的核心部件被整合到了SRI International開(kāi)發(fā)的定理證明器PVS中.Yices2對(duì)Yices進(jìn)行了優(yōu)化和改進(jìn)，減少了復(fù)雜類(lèi)型的數(shù)量，只含有整數(shù)、實(shí)數(shù)、位向量和布爾變量4種原子類(lèi)型并簡(jiǎn)化了類(lèi)型的表示，例如將int(整數(shù))類(lèi)型視為real(實(shí)數(shù))類(lèi)型的子類(lèi)型.Yices2提供了符合SMT-LIB標(biāo)準(zhǔn)的接口，增加了對(duì)元組和標(biāo)量等數(shù)據(jù)類(lèi)型的支持.

其他SMT求解器也都有各自的特點(diǎn).例如，Barcelogic的核心求解算法為Ackerman方法、DTC方法以及位移等式策略.MathSAT4在結(jié)合了Ackerman方法和DTC方法的基礎(chǔ)上，使用了動(dòng)態(tài)Ackerman方法求解可滿(mǎn)足性問(wèn)題.Boolector可以求解含有位向量理論和可擴(kuò)展的數(shù)組理論的可滿(mǎn)足性問(wèn)題.VeriT是基于改進(jìn)的Nelson-Oppen方法開(kāi)發(fā)的SMT求解器，僅支持無(wú)量詞理論和整數(shù)差分理論的可滿(mǎn)足性問(wèn)題求解.

為了推動(dòng)SMT求解技術(shù)及SMT求解器的進(jìn)步，可滿(mǎn)足性理論及應(yīng)用國(guó)際學(xué)術(shù)年會(huì)自2005年開(kāi)始，每年舉辦SMT-COMP競(jìng)賽，到2015年為止共成功舉辦了11屆比賽.用于評(píng)判各個(gè)求解器求解能力的標(biāo)準(zhǔn)測(cè)試集來(lái)源于SMT-LIB，其數(shù)量從最初的1 400個(gè)增加到如今的10 000多個(gè).標(biāo)準(zhǔn)測(cè)試集是由各個(gè)背景理論測(cè)試集組成的，例如線(xiàn)性算數(shù)測(cè)試集(LIA)、位向量(QF_BV)測(cè)試集等.表1包含了自2005年開(kāi)始到目前為止每一屆SMT-COMP的比賽結(jié)果.表1以每個(gè)SMT求解器所支持背景理論的數(shù)量、在不同背景理論測(cè)試集上的排名以及綜合評(píng)分作為依據(jù)，在Winner一欄中列出了每一屆比賽的冠軍，并在Background Theories一欄中給出了對(duì)應(yīng)SMT求解器在參賽時(shí)所用到的背景理論測(cè)試集，在這些測(cè)試集上該SMT求解器綜合的求解效率要好于其他SMT求解器.由表1可以看出，Barcelogic獲得了第1屆競(jìng)賽的冠軍，并在QF_UF等4個(gè)背景理論測(cè)試集上有著突出的表現(xiàn).在隨后的比賽中，Yices和Yices2也獲得了冠軍，支持背景理論的數(shù)量遠(yuǎn)遠(yuǎn)大于Barcelogic.在SMT-COMP2010中，CVC3也取得了不錯(cuò)的成績(jī).最近5年中，Z3始終排在第1位，支持背景理論的數(shù)量也在逐年增加，在大多數(shù)理論測(cè)試集上的求解速度快于其他求解器，綜合性能較好.

Table 1 Winners of the Each SMT-COMP Editions表1 歷屆SMT-COMP的冠軍

表2是2015年SMT-COMP的比賽結(jié)果，Sequential Performances代表順序性能的評(píng)分，Parallel Performances代表并行性能的評(píng)分，Normal和Industrail分別代表各個(gè)SMT求解器在標(biāo)準(zhǔn)測(cè)試集和工業(yè)測(cè)試集上的評(píng)分，以求解速度、支持的背景理論數(shù)量等因素為依據(jù)，在Rank一欄中給出了每個(gè)求解器的綜合排名.

Table 2 Ranking of SMT-COMP 2015表2 SMT-COMP2015綜合排名

由表2可以看出，無(wú)論是在標(biāo)準(zhǔn)集測(cè)試上還是在工業(yè)測(cè)試集上測(cè)試，Z3求解器的綜合性能都要比其他SMT求解器好.Z3在標(biāo)準(zhǔn)測(cè)試集和工業(yè)測(cè)試集上的評(píng)分相同，說(shuō)明Z3具有較好的穩(wěn)定性，Z3的Sequential Performance的評(píng)分高于Parallel Performance的評(píng)分.排名第2的CVC4的評(píng)分與Z3相差不大，唯一的區(qū)別是在標(biāo)準(zhǔn)測(cè)試集和工業(yè)測(cè)試集上Parallel Performance的評(píng)分都略高于Sequential Performance的評(píng)分，是為數(shù)不多的在Parallel Performance的評(píng)分上取得較好成績(jī)的求解器之一.Yices和MathSAT求解器評(píng)分低于Z3和CVC4，在2個(gè)測(cè)試集上的Sequential Performance的評(píng)分和Parallel Performance的評(píng)分均保持不變，較為穩(wěn)定.CVC3和Boolecter的評(píng)分與其他求解器相差過(guò)大，無(wú)論是在標(biāo)準(zhǔn)測(cè)試集上還是在工業(yè)測(cè)試集上，求解大規(guī)?？蓾M(mǎn)足性問(wèn)題的能力都要低于其他求解器.

在2015年SMT-COMP中，舉辦方提供了40種不同的背景理論測(cè)試集，基于每個(gè)SMT求解器在各個(gè)測(cè)試集上的綜合評(píng)分，表3給出了主流SMT求解器在不同背景理論測(cè)試集中的排名.其中LIA表示整數(shù)線(xiàn)性算數(shù)理論，QF_ABV表示無(wú)量詞固定位向量數(shù)組理論，QF_IDL表示無(wú)量詞整數(shù)差分邏輯理論，QF_NIA表示無(wú)量詞整數(shù)非線(xiàn)性算數(shù)理論，QF_UFLIA表示無(wú)量詞未解釋函數(shù)的整數(shù)線(xiàn)性算數(shù)理論，“ ”代表此SMT求解器不支持對(duì)應(yīng)理論的求解.從表3中可以看出，Z3求解器支持主流的背景理論數(shù)量最多.

Table 3 Ranking of SMT Solvers Based on Different Background Theory’s (SMT-COMP 2015)表3 不同背景理論下的SMT求解器排名 (SMT-COMP 2015)

4 SMT應(yīng)用

隨著SMT判定算法的不斷發(fā)展以及SMT求解器的逐漸成熟，人們開(kāi)始使用SMT解決一些實(shí)際問(wèn)題，例如測(cè)試用例自動(dòng)生成、程序缺陷檢測(cè)、RTL驗(yàn)證、程序分析與驗(yàn)證、線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解等.

4.1 測(cè)試用例自動(dòng)生成

4.1.1 基于SMT的測(cè)試用例自動(dòng)生成

測(cè)試用例自動(dòng)生成是設(shè)計(jì)和編寫(xiě)軟件測(cè)試用例一種方法，也是軟件測(cè)試的一種重要手段，常用于檢測(cè)程序缺陷.基于SMT的測(cè)試用例自動(dòng)生成技術(shù)主要分為獲取程序執(zhí)行路徑和檢查路徑可滿(mǎn)足性這2個(gè)部分.獲取程序的執(zhí)行路徑主要依賴(lài)于動(dòng)態(tài)符號(hào)執(zhí)行，即在不執(zhí)行程序的前提下，使用具體數(shù)值代替程序變量作為程序的輸入，模擬程序的執(zhí)行，分析1條指定路徑會(huì)觸發(fā)程序中哪些代碼的執(zhí)行，并記錄下此路徑.檢查路徑可滿(mǎn)足性需要將程序執(zhí)行路徑轉(zhuǎn)化為SMT公式，然后使用SMT求解器判斷公式的可滿(mǎn)足性.具體思想如下：首先利用基于動(dòng)態(tài)符號(hào)執(zhí)行的代碼模擬執(zhí)行器模擬一條具體的程序執(zhí)行路徑，同時(shí)記錄路徑中的條件語(yǔ)句和賦值語(yǔ)句，再通過(guò)SMT背景理論將這些語(yǔ)句轉(zhuǎn)化為SMT公式F，例如可以用未解釋函數(shù)背景理論將賦值語(yǔ)句表示為等式的合取形式，而數(shù)組賦值語(yǔ)句則需要數(shù)組理論的支持，利用SMT求解器對(duì)判斷F的可滿(mǎn)足性，此時(shí)會(huì)出現(xiàn)2種情況：

1) 如果F可滿(mǎn)足，F(xiàn)的具體可滿(mǎn)足性賦值可作為該條路徑的輸入(測(cè)試用例).通過(guò)修改F中的某個(gè)條件，例如將分支語(yǔ)句if(a=0)中的表達(dá)式(a=0)改為(a!=0)，可以構(gòu)建出1條新的執(zhí)行路徑，將新的路徑轉(zhuǎn)化為公式F′，通過(guò)SMT求解器求解F′，得到新的輸入(測(cè)試用例)，利用新的輸入再進(jìn)行新一輪的路徑構(gòu)造、約束求解.通過(guò)這種迭代的路徑生成方法，動(dòng)態(tài)符號(hào)執(zhí)行可以持續(xù)遍歷程序的可執(zhí)行路徑，直到所得到的測(cè)試用例數(shù)量達(dá)到預(yù)期值，從而實(shí)現(xiàn)了測(cè)試用例的自動(dòng)生成.

2) 當(dāng)F不可滿(mǎn)足時(shí)，說(shuō)明當(dāng)前執(zhí)行路徑不正確，修改某一分支語(yǔ)句的分支條件后進(jìn)行新一輪的路徑構(gòu)造、約束求解.

4.1.2 具體示例

圖3(a)中函數(shù)addition()是1個(gè)加法函數(shù)，函數(shù)輸入choice的不同取值會(huì)產(chǎn)生不同的執(zhí)行路徑，從而影響sum的取值.圖3(b)是addition()的2條執(zhí)行路徑.

基于SMT的測(cè)試用例自動(dòng)生成的過(guò)程如下：首先使用代碼模擬執(zhí)行器得到addition()的1條執(zhí)行路徑，即圖3(b)中的路徑1，將路徑1轉(zhuǎn)化為SMT公式，記為

F1=(a=0)∧(choice>1)∧(sum=2)，

(9)

利用SMT求解器判斷出F1是可滿(mǎn)足的，且可滿(mǎn)足解為(choice=2)，從而得到了第1個(gè)測(cè)試用例.然后將if語(yǔ)句中的表達(dá)式取反，得到圖3(b)中的路徑2，將路徑2轉(zhuǎn)化為SMT公式，記為

F2=(a=0)∧(choice≤1)∧(sum=2)，

(10)

利用SMT求解器判斷出F2是可滿(mǎn)足的，且可滿(mǎn)足解為(choice=1)，達(dá)到了測(cè)試用例自動(dòng)生成的目的.

Fig. 3 Record the number of requests
圖3 記錄請(qǐng)求次數(shù)

4.1.3 SMT在測(cè)試用例自動(dòng)生成中的應(yīng)用

許多成熟的工具中都用到了基于SMT的測(cè)試用例自動(dòng)生成方法，例如Pex[39]工具將.Net組件和基于SMT的測(cè)試用例自動(dòng)生成技術(shù)相結(jié)合，使用Z3求解路徑的可滿(mǎn)足性，可以自動(dòng)生成.Net程序的測(cè)試用例，例如C#程序.Pex也為含有復(fù)雜數(shù)據(jù)結(jié)構(gòu)的程序提供測(cè)試用例自動(dòng)生成的功能.

SAGE[85]是1個(gè)白盒測(cè)試工具，使用代碼覆蓋率檢查工具Nirvana和約束產(chǎn)生工具TruScan將程序路徑轉(zhuǎn)化為SMT公式，利用Z3求解公式的可滿(mǎn)足性并自動(dòng)生成新的測(cè)試用例，結(jié)合微軟模糊測(cè)試的基礎(chǔ)框架，SAGE可以找出程序中的大多數(shù)錯(cuò)誤.

JPF-SE[86]工具利用符號(hào)執(zhí)行技術(shù)獲取程序的執(zhí)行路徑并轉(zhuǎn)化為SMT公式，使用Yices求解路徑的可滿(mǎn)足性并生成測(cè)試用例并作為輸入提供給工具內(nèi)的其他組件.

Yogi[82]是1個(gè)基于SMT的C語(yǔ)言靜態(tài)分析和測(cè)試工具，該工具使用Z3求解程序路徑的可滿(mǎn)足性并產(chǎn)生測(cè)試用例，被集成到微軟的靜態(tài)驅(qū)動(dòng)檢測(cè)框架中，完成了69個(gè)Windows Vista的驅(qū)動(dòng)檢測(cè)工作.

Arcaini等人[87]提出了一種使用區(qū)分配置(dis-tinguishing configuration)檢查特征模型錯(cuò)誤的方法.該方法利用Yices求解測(cè)試謂詞(test predicate)的可滿(mǎn)足性，如果可滿(mǎn)足，則具體的可滿(mǎn)足賦值即為區(qū)分配置(distinguishing configuration)，使用區(qū)分配置作為測(cè)試用例進(jìn)行特征模型的錯(cuò)誤檢查工作，實(shí)現(xiàn)了測(cè)試用例的自動(dòng)生成;如果不可滿(mǎn)足，則產(chǎn)生特征模型的突變(mutated)模型.

4.2 程序缺陷檢測(cè)

4.2.1 基于SMT的程序缺陷檢測(cè)

程序缺陷檢測(cè)的目的是檢查程序是否違反了給定的安全屬性，例如是否有死鎖、是否存在安全漏洞等.軟件測(cè)試是檢測(cè)嵌入式程序缺陷的一種常用方法，所需的測(cè)試用例可以由人工編寫(xiě)或者使用動(dòng)態(tài)符號(hào)執(zhí)行等技術(shù)自動(dòng)生成.當(dāng)程序規(guī)模很大時(shí)，很難獲取覆蓋程序所有執(zhí)行路徑的全部測(cè)試用例，時(shí)間開(kāi)銷(xiāo)也是難以接受的.因此，軟件測(cè)試只適用于尋找軟件的缺陷，無(wú)法保證程序不含有某個(gè)指定的缺陷.基于模型檢測(cè)[88]的程序缺陷檢測(cè)方法是一種自動(dòng)檢測(cè)技術(shù)，通過(guò)對(duì)程序進(jìn)行抽象得到1個(gè)有限的狀態(tài)空間，減少了缺陷檢測(cè)帶來(lái)的時(shí)間開(kāi)銷(xiāo)，在一定程度上減小了缺陷檢測(cè)的難度.但是程序規(guī)模的不斷增大導(dǎo)致?tīng)顟B(tài)空間也隨之增大，狀態(tài)空間爆炸是模型檢測(cè)不可避免的問(wèn)題.

基于SMT的有界模型檢測(cè)(bounded model checking，BMC)方法成為了新的研究熱點(diǎn).主要思想是檢測(cè)程序在界限K內(nèi)是否滿(mǎn)足給定的安全屬性(property)，給定系統(tǒng)I，1個(gè)安全屬性P，以及1個(gè)界限(bound)K，BMC會(huì)將系統(tǒng)I展開(kāi)K次得到驗(yàn)證條件V，V是可滿(mǎn)足的當(dāng)且僅當(dāng)P在界限K內(nèi)有1個(gè)反例.這里的界限K是指將源程序中的循環(huán)結(jié)構(gòu)(比如for循環(huán))展開(kāi)K次.V是源程序所轉(zhuǎn)化成的等價(jià)SMT公式F.基于SMT的有界模型檢測(cè)是指將上述F與P的反(F∧P)送入SMT求解器，如果(F∧P)可滿(mǎn)足，證明程序的某一條執(zhí)行路徑會(huì)違反安全屬性，通過(guò)SMT求解器返回的具體可滿(mǎn)足賦值可以得到使得程序出錯(cuò)的具體輸入，如果(F∧P)不可滿(mǎn)足，則證明程序在界限K內(nèi)不違反安全屬性.

4.2.2 具體示例

下面用1個(gè)例子說(shuō)明SMT求解器在程序缺陷檢測(cè)中的應(yīng)用.圖4(a)是1個(gè)C語(yǔ)言程序，其功能是計(jì)算斐波那契數(shù)列第n項(xiàng)的數(shù)值，并將結(jié)果存在整型數(shù)組result[0]中.斐波那契數(shù)列是指這樣1個(gè)數(shù)列：數(shù)列的第0項(xiàng)為0，第1項(xiàng)為1，第2項(xiàng)為1，并且從第2項(xiàng)起，每一項(xiàng)都是前2項(xiàng)的數(shù)字之和，例如，斐波那契數(shù)列的前6項(xiàng)為：0，1，1，2，3，5.圖4(b)表示函數(shù)Fib(intn)的靜態(tài)單賦值(static single assignment, SSA)形式，SSA形式與源程序的區(qū)別在于2點(diǎn)：1)SSA形式中的每個(gè)變量名僅被賦值1次.對(duì)于同一變量的多次賦值采用“原變量名+賦值次數(shù)”的形式來(lái)取代原變量名;2)SSA形式中消去了原程序中的循環(huán)結(jié)構(gòu)(比如while)，利用循環(huán)體展開(kāi)的形式等價(jià)表示循環(huán)結(jié)構(gòu).圖4(b)是將源程序中的while循環(huán)展開(kāi)3次的結(jié)果.圖4(c)是將SSA形式中的語(yǔ)句進(jìn)行合取得到的等價(jià)表示形式，稱(chēng)為SMT公式F.程序中存在數(shù)組result，需要檢查是否存在數(shù)組越界問(wèn)題，由于數(shù)組只含有1個(gè)元素，因此安全屬性P可以被表示為(j=0).SMT求解器將邏輯公式(F∧P)作為輸入，通過(guò)結(jié)合相應(yīng)的背景理論(例如本程序需要用到未解釋函數(shù)理論)對(duì)公式F的可滿(mǎn)足性進(jìn)行求解，可知(F∧P)不可滿(mǎn)足，程序不存在數(shù)組越界問(wèn)題，沒(méi)有違反給定的安全屬性.

Fig. 4 Converting the source code into the SMT formula
圖4 源程序轉(zhuǎn)化為SMT公式

4.2.3 SMT在程序缺陷檢測(cè)中的應(yīng)用

基于SMT的有界模型檢測(cè)方法中的界限K使得此方法在醫(yī)療、通信等嵌入式程序的驗(yàn)證中有著很大的優(yōu)勢(shì).原因在于相對(duì)于一般軟件，嵌入式程序的代碼量小，且嵌入式程序不鼓勵(lì)使用大量的遞歸和循環(huán)語(yǔ)句，很少見(jiàn)到循環(huán)次數(shù)超過(guò)K的循環(huán)體，只需要證明程序在K步內(nèi)滿(mǎn)足安全屬性即可.

Cordeiro等人[7]在2012年提出了一種基于有界模型檢測(cè)的嵌入式軟件缺陷檢測(cè)方法.此方法先將嵌入式程序的ANSI-C語(yǔ)言源文件轉(zhuǎn)化為控制流圖(control flow graph，CFG)，再把CFG對(duì)應(yīng)的GOTO-Program轉(zhuǎn)化為SSA形式，對(duì)SSA進(jìn)行處理并提取出用戶(hù)斷言和安全屬性后得到與源程序等價(jià)的SMT公式，然后使用Z3或者Boolecter求解公式的可滿(mǎn)足性，根據(jù)求解結(jié)果判定該嵌入式程序是否滿(mǎn)給定的安全屬性.此方法在軟件ESBMC(efficient SMT-based context-bounded model checker)中得以實(shí)現(xiàn)，圖5是ESBMC的結(jié)構(gòu)圖，描述了ESBMC進(jìn)行有界模型檢測(cè)的步驟.ESBMC支持ANSI-C語(yǔ)言中許多數(shù)據(jù)結(jié)構(gòu)、變量的檢查，其中包括標(biāo)量數(shù)據(jù)類(lèi)型(比如整型、長(zhǎng)整型等)、固定點(diǎn)算數(shù)、算術(shù)溢出、數(shù)組、結(jié)構(gòu)體、指針、動(dòng)態(tài)內(nèi)存分配等.ESBMC會(huì)將它們轉(zhuǎn)化為與SMT背景理論相符合的公式，再將公式送入SMT求解器求解.

Fig. 5 Overview of the ESBMC architecture圖5 ESBMC結(jié)構(gòu)概覽

Ramalho等人[89]在2013年提出了基于SMT的C++程序缺陷檢測(cè)方法，可以檢測(cè)C++語(yǔ)言中的標(biāo)準(zhǔn)庫(kù)函數(shù)以及C++特有的模板、容器、繼承、異常的缺陷.C++庫(kù)函數(shù)在有界模型檢測(cè)中會(huì)產(chǎn)生大量復(fù)雜而又冗余的驗(yàn)證條件，因此，Ramalho等人[89]為C++的庫(kù)函數(shù)建立C++操作模型(C++ operational model， COM)，作為C++庫(kù)函數(shù)的簡(jiǎn)單表示，在保證有界模型檢測(cè)的正確性的同時(shí)減少了產(chǎn)生的驗(yàn)證條件的數(shù)量，并使用Z3等SMT求解器判定驗(yàn)證條件的可滿(mǎn)足性，提高了驗(yàn)證效率.COM中包含ANSI-C庫(kù)函數(shù)，保證了對(duì)ANSI-C語(yǔ)言檢測(cè)的支持.

Cordeiro等人[90-91]提出了基于SMT的多線(xiàn)程軟件上下文界限模型檢測(cè)方法，可以檢測(cè)多線(xiàn)程軟件的缺陷.文中把多線(xiàn)程并發(fā)視為以不同順序激活不同線(xiàn)程的線(xiàn)性序列，將程序的所有可達(dá)狀態(tài)記為狀態(tài)空間W，將線(xiàn)性序列、可達(dá)狀態(tài)已經(jīng)安全屬性轉(zhuǎn)化為SMT公式，利用Z3等SMT求解器求解公式的可滿(mǎn)足性，判斷每一個(gè)狀態(tài)是否會(huì)違反安全屬性.通過(guò)可達(dá)樹(shù)(reachability tree， RT)、惰性方法(lazy approach)、調(diào)度算法以及下近似和展開(kāi)方法(under-approximation and widening approach)完成了多線(xiàn)程軟件的模型檢測(cè)工作.文中還對(duì)Pthread library[92]進(jìn)行了建模，包括互斥鎖操作、條件等待等操作.

Pereira等人[93]在2016年提出了基于SMT的統(tǒng)一計(jì)算設(shè)備架構(gòu)(computer unified device architecture，CUDA)程序上下文界限模型檢測(cè)方法，CUDA是由NVIDA[94]開(kāi)發(fā)的1個(gè)并行編程平臺(tái)和應(yīng)用編程接口模型，目的是為了充分利用GPU(graphics processing unit)的能力.他們?cè)贓SBMC的基礎(chǔ)上開(kāi)發(fā)了ESBMC-GPU，能很好地對(duì)CUDA函數(shù)庫(kù)進(jìn)行建模，并利用SMT進(jìn)行模型檢測(cè)工作.為了緩解多線(xiàn)程環(huán)境下?tīng)顟B(tài)復(fù)雜的問(wèn)題，他們將單調(diào)偏序規(guī)約(monotonic partial order reduction，MPOR)應(yīng)用到CUDA程序中來(lái)消除冗余的程序執(zhí)行路徑和RT[95]中的冗余狀態(tài).

基于SMT的模型檢測(cè)工具在工業(yè)界也得到了應(yīng)用，Ball等人[96]使用SLAM工具對(duì)Windows NT驅(qū)動(dòng)程序進(jìn)行了模型檢測(cè)工作，檢測(cè)了其中是否存在死鎖等問(wèn)題.

4.3 RTL驗(yàn)證

4.3.1 基于SMT的RTL驗(yàn)證

RTL驗(yàn)證是檢驗(yàn)集成電路功能性錯(cuò)誤的方法.隨著集成電路規(guī)模的不斷增大，普通模擬驗(yàn)證已經(jīng)無(wú)法滿(mǎn)足大規(guī)模集成電路驗(yàn)證的需要，因此，形式化驗(yàn)證受到了高度的關(guān)注.目前工業(yè)界采用了一些SAT求解器處理求解門(mén)級(jí)電路的問(wèn)題，比如Minisat和BerkMin等.研究人員也對(duì)SAT求解器在電子電路驗(yàn)證中的應(yīng)用做了相關(guān)研究[97]，并提出了自動(dòng)測(cè)試圖樣產(chǎn)生(automatic test pattern generation, ATPG)、整數(shù)線(xiàn)性規(guī)劃(integer linear programming, ILP)、超圖劃分等求解方法[98].但是這些方法求解門(mén)級(jí)電路所需要的時(shí)間開(kāi)銷(xiāo)讓人難以接受，因此，基于SMT的RTL混合可滿(mǎn)足性求解方法是目前的研究熱點(diǎn).

4.3.2 具體示例

下面用1個(gè)簡(jiǎn)單的例子來(lái)說(shuō)明SMT在RTL驗(yàn)證中的應(yīng)用.如圖6所示,電路E只含有1個(gè)與門(mén)和1個(gè)或門(mén)，需要驗(yàn)證是否存在1組輸入使得電路輸出結(jié)果Z為1(真).具體步驟如下：首先根據(jù)電路圖結(jié)構(gòu)將E轉(zhuǎn)化為等價(jià)的SMT公式F=(a∧b)∨c，再利用SMT求解器求解F的可滿(mǎn)足性，可知當(dāng)a=1，b=1，c=0時(shí)，F(xiàn)可滿(mǎn)足:即Z=1，達(dá)到了驗(yàn)證的目的.

Fig. 6 Circuit diagram E圖6 電路圖E

4.3.3 SMT在RTL驗(yàn)證中的應(yīng)用

許多形式化驗(yàn)證工具，包括一些工業(yè)界采用的工具都是通過(guò)位級(jí)模型實(shí)現(xiàn)RTL驗(yàn)證，主要思想是將高層級(jí)的RTL設(shè)計(jì)轉(zhuǎn)化為位級(jí)信息，再對(duì)位級(jí)信息進(jìn)行展開(kāi)驗(yàn)證工作.這種方法不能充分利用高層級(jí)所含的結(jié)構(gòu)，在轉(zhuǎn)換中會(huì)丟失高層級(jí)的信息，可擴(kuò)展性低.

Kroening等人[99]提出了一種利用高層級(jí)信息模型進(jìn)行RTL驗(yàn)證的方法，該方法利用謂詞抽象技術(shù)和SMT求解器進(jìn)行位級(jí)以及字級(jí)的驗(yàn)證(word-level verification).結(jié)合了反例指導(dǎo)的抽象框架[100](counterexample guided abstraction refinement frame)的謂詞抽象技術(shù)將系統(tǒng)的實(shí)際狀態(tài)空間映射到1個(gè)抽象的、狀態(tài)數(shù)較少的空間中，并在系統(tǒng)表現(xiàn)出的特性上與原有系統(tǒng)保持一致.圖7是RTL Verilog謂詞抽象技術(shù)的大體框架.

Fig. 7 The predicate abstraction techniques of RTL verilog圖7 RTL verilog的謂詞抽象技術(shù)

Puri等人[101]提出了基于SMT的自動(dòng)RTL測(cè)試生成器SI-SMART(swarm intelligence-SMART)，目的是解決傳統(tǒng)有界模型檢測(cè)方法和基于符號(hào)執(zhí)行的檢測(cè)方法對(duì)循環(huán)處理能力不足的問(wèn)題.在DUT(design under test)中，循環(huán)是很常見(jiàn)的，但是有界模型檢測(cè)或者基于符號(hào)執(zhí)行的檢測(cè)方法只能將循環(huán)展開(kāi)至多K次，再進(jìn)行RTL驗(yàn)證工作.此方法不適用于DUT.SI-SMART先對(duì)DUT中的循環(huán)進(jìn)行抽象，再找出直接或間接影響目標(biāo)分支條件的變量，分析它們之間的遞推關(guān)系技術(shù)并以此消除控制流圖中的循環(huán)展開(kāi)，從而解決了需要按照一定界限展開(kāi)循環(huán)的問(wèn)題.

Brady等人[102]提出了硬件設(shè)計(jì)的自動(dòng)項(xiàng)級(jí)(term-level)抽象技術(shù)，是一種基于形式化邏輯的、針對(duì)字級(jí)設(shè)計(jì)的抽象技術(shù)，所有數(shù)據(jù)用抽象的項(xiàng)、功能函數(shù)和未解釋函數(shù)等形式表達(dá)，解決了目前大多數(shù)抽象技術(shù)所面臨的抽象等價(jià)性問(wèn)題，即是否可以把組件C等價(jià)的抽象為另一個(gè)表示C′.此抽象技術(shù)先利用隨機(jī)模擬技術(shù)檢驗(yàn)功能模塊是否可以用未解釋函數(shù)來(lái)抽象，再利用靜態(tài)分析技術(shù)計(jì)算抽象條件，最后利用SMT求解器驗(yàn)證項(xiàng)級(jí)抽象結(jié)果的可滿(mǎn)足性.目前這種技術(shù)已經(jīng)成功的應(yīng)用于處理器設(shè)計(jì)驗(yàn)證、接口邏輯驗(yàn)證等領(lǐng)域.

趙燕妮等人[103]利用SMT求解RTL的可滿(mǎn)足性問(wèn)題，其主要思想是將RTL電路視為1個(gè)超圖，然后基于超圖劃分的方法得到1個(gè)割集最小的等量超圖劃分，形成有限個(gè)超圖子問(wèn)題，再利用Yices求解子問(wèn)題的可滿(mǎn)足性.

Gent等人[104]提出了基于有界模型檢測(cè)和群體智能的RTL功能測(cè)試方法，該方法使用HYBRO[105](hybrid analysis and branch coverage optimizations)抽取特定的程序執(zhí)行路徑并將其轉(zhuǎn)化SMT公式，利用Z3求解這些SMT公式的可滿(mǎn)足性，再結(jié)合有界模型檢測(cè)的方法進(jìn)行RTL驗(yàn)證.

Kunapareddy等人[10]對(duì)LPSAT和SMT在RTL驗(yàn)證中的應(yīng)用進(jìn)行了比較，結(jié)論表明：基于Z3的RTL驗(yàn)證方法在代碼復(fù)雜度、執(zhí)行時(shí)間和迭代次數(shù)上的表現(xiàn)均優(yōu)于LPSAT方法.

4.4 程序分析與驗(yàn)證

4.4.1 基于SMT的程序分析與驗(yàn)證

基于SMT的程序分析與驗(yàn)證是一種形式化方法，基礎(chǔ)思想來(lái)源于Floyd和Hoare提出的弗洛伊德-霍爾邏輯(Floyd-Hoare logic).該方法將前置條件(pre-condition)、循環(huán)不變量(loop invariant)和后置條件(post-condition)以斷言(assert)的形式引入程序驗(yàn)證中，三者分別判斷程序在運(yùn)行前、運(yùn)行中以及運(yùn)行結(jié)束時(shí)的正確性，通過(guò)判定斷言得成立情況檢驗(yàn)程序的正確性.

4.4.2 具體示例

用1個(gè)簡(jiǎn)單的程序來(lái)說(shuō)明SMT在程序分析與驗(yàn)證中的應(yīng)用.圖8(a)是1個(gè)求最大公約數(shù)的程序GCD，x和y是程序的輸入，m是程序中的輔助變量.為該程序加上pre-condition，loop invariant以及post-condition后得到的程序如圖8(b)所示.具體過(guò)程如下：1)程序GCD的2個(gè)輸入為正數(shù)是求解最大公約數(shù)的基本條件，即F1=(x≥0)∧(y>0).運(yùn)算過(guò)程中的被除數(shù)要大于除數(shù)，即F2=(x≥y).將F1和F2加入到pre-condition中.2)在while循環(huán)中，x，y和m需要恒大于0且x要始終大于等于y，即F3=(x≥0)∧(y>0)∧(x≥y)∧(m≥0)，將F3加入到loop invariant中.3)最大公約數(shù)是1個(gè)整數(shù)，即F4=(y≥0)，將F4加入到post-condition中.然后通過(guò)動(dòng)態(tài)符號(hào)執(zhí)行技術(shù)遍歷程序GCD的所有執(zhí)行路徑，再將這些路徑轉(zhuǎn)化為SMT公式F，然后將pre-condition，loop invariant以及post-condition轉(zhuǎn)化為SMT公式并與F合并，記為F′，通過(guò)SMT求解器求解F′的可滿(mǎn)足性，若F′不可滿(mǎn)足，說(shuō)明程序中含有錯(cuò)誤，若F′可滿(mǎn)足，說(shuō)明在所有斷言得到滿(mǎn)足性的情況下，程序是正確的，驗(yàn)證了程序的部分正確性.本例中的程序GCD是正確的.

Fig. 8 Greatest common divisor program
圖8 求最大公約數(shù)程序

4.4.3 SMT在程序分析與驗(yàn)證中的應(yīng)用

2005年，Leroy[15]研發(fā)了1個(gè)C語(yǔ)言編譯器CompCert，該編譯器是經(jīng)過(guò)形式化驗(yàn)證的優(yōu)化編譯器，主要功能是將C語(yǔ)言編譯為PowerPC匯編代碼，Leroy對(duì)編譯的每一步操作給出了嚴(yán)格的數(shù)學(xué)證明，大大提高了CompCert的可信度.但是這種基于數(shù)學(xué)證明的程序分析與驗(yàn)證方法難度大、耗時(shí)長(zhǎng)，因此，基于SMT的程序分析與驗(yàn)證成為了新的研究熱點(diǎn).

何炎祥等人[106]提出了使用SMT求解器進(jìn)行路徑敏感程序驗(yàn)證的方法，主要思想是通過(guò)最大強(qiáng)連通分量壓縮循環(huán)路徑并使用基于布爾表達(dá)式的方法對(duì)路徑空間進(jìn)行抽象，減少了待驗(yàn)證程序路徑的規(guī)模，再結(jié)合動(dòng)態(tài)符號(hào)執(zhí)行技術(shù)和抽象解釋技術(shù)將壓縮后的程序路徑轉(zhuǎn)化為SMT公式，使用Z3求解公式的可滿(mǎn)足性，如果可滿(mǎn)足，證明路徑是正確的，達(dá)到了程序驗(yàn)證的目的，否則說(shuō)明路徑會(huì)觸發(fā)程序的某個(gè)錯(cuò)誤.

在計(jì)算機(jī)編程中，需要在編譯前確定變量的類(lèi)型(例如float或double)，變量精度會(huì)受到類(lèi)型的影響，在程序輸入不變的情況下，改變變量類(lèi)型在某些情況下會(huì)使程序輸出不同的結(jié)果.但是，在程序運(yùn)行之前很難判斷所選變量類(lèi)型是否符合計(jì)算的精度.Paganelli等人[107]提出了一種通過(guò)增加精確度驗(yàn)證浮點(diǎn)數(shù)程序穩(wěn)定性的方法，證明了增加變量精度會(huì)使得結(jié)果產(chǎn)生微小的變化.該方法首先分析程序中變量的類(lèi)型以及用戶(hù)的斷言，計(jì)算出程序的最弱前置條件(weakest precondition)，然后將最弱前置條件轉(zhuǎn)化為SMT公式F并使用Z3求解F的可滿(mǎn)足性，如果F可滿(mǎn)足，則具體的可滿(mǎn)足賦值可以作為程序的1個(gè)測(cè)試用例，作為后續(xù)證明過(guò)程的輸入.如果不可滿(mǎn)足，便需要用戶(hù)對(duì)程序進(jìn)行調(diào)整.

克雷格插值(craig interpolation)方法在程序驗(yàn)證領(lǐng)域取得了不錯(cuò)的成績(jī)，例如Kroening等人[108]開(kāi)發(fā)了基于克雷格插值的軟件驗(yàn)證工具Wolverine.但當(dāng)插值規(guī)模很大時(shí)，程序驗(yàn)證的效率可能會(huì)受到影響，因此Pigorsch等人[109]提出了一種基于SMT的減小interpolation規(guī)模的算法，可以提升克雷格插值方法的效率，MathSAT負(fù)責(zé)算法中公式的不可滿(mǎn)足性的證明工作.

工業(yè)界的驗(yàn)證工具也用到了SMT求解器，例如，VCC[110](verifying C compiler)是1個(gè)低層級(jí)并發(fā)系統(tǒng)(low-level concurrent system)代碼驗(yàn)證工具，集成了SMT求解器Z3，可以根據(jù)程序中的注釋(比如函數(shù)功能、狀態(tài)斷言等)驗(yàn)證程序的正確性.微軟使用VCC驗(yàn)證了虛擬化產(chǎn)品Hyper -V的正確性.

4.5 線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解

4.5.1 SMT與線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解

SMT在線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解中的主要應(yīng)用是：結(jié)合背景理論(例如線(xiàn)性實(shí)數(shù)理論)，利用SMT求解器找到滿(mǎn)足目標(biāo)公式及約束條件的最優(yōu)解.具體來(lái)說(shuō)，首先根據(jù)實(shí)際問(wèn)題的約束條件和優(yōu)化目標(biāo)抽象出約束表達(dá)式φ和目標(biāo)函數(shù)H，再利用SMT求解器求出滿(mǎn)足φ的可行解集G，然后找出G中使H達(dá)到最大值(或最小值)的可行解，即為最優(yōu)解.

4.5.2 具體示例

結(jié)合Li等人[111]提出的基于SMT的線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解方法，舉1個(gè)簡(jiǎn)單的例子，給定基于線(xiàn)性實(shí)數(shù)算術(shù)理論的公式:

φ≡(1≤y≤3)∧(1≤x≤3∨x≥4)，

(11)

其中，φ的可行域表示二維坐標(biāo)系上的一片區(qū)域，x和y均為實(shí)數(shù)變量，分別位于坐標(biāo)系的橫軸和縱軸上，(x,y)代表坐標(biāo)系中的1個(gè)點(diǎn)記為p=(x,y).目標(biāo)函數(shù)為H={y,x+y}.需要在滿(mǎn)足約束條件φ的情況下求出使目標(biāo)函數(shù)H達(dá)到最大值的x和y，即(xopt,yopt)，基于SMT的線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解步驟如下：

1) 假設(shè)最優(yōu)解為optT(φ)，根據(jù)約束條件φ可將最優(yōu)解的最小上界(under-approximation， UA)初始化為

UA≡y≤-∞∧x+y≤-∞，

(12)

最大上界(over-approximation， OA)初始化為

OA≡y≤∞∧x+y≤∞.

(13)

2) 將φ∧UA送入SMT求解器，求得可行解為(x=2)∧(y=2)，記為p1=(2,2)，更新最小上界為

UA≡y≤2∧x+y≤4，

更新最大上界為

OA≡y≤3.

3) 將φ中每個(gè)原子公式中的不等號(hào)替換為等號(hào)，得到的集合記為

ε(φ)={l=k|l≤k∈φ}，

例如，此時(shí)ε(φ)={x=1,x=3,x=4,y=1,y=3}.點(diǎn)p的邊界類(lèi)定義為[p]=e∈ε(φ)|p|=e.[p1]=?，因?yàn)榇它c(diǎn)不接觸任一邊界.提取目標(biāo)函數(shù)H的第1個(gè)元素y，判斷在滿(mǎn)足y≤3的基礎(chǔ)上，是否存在優(yōu)于可行解p1的另1個(gè)可行解p2，即:

S≡[p1]?[p2]∧y(p2)≥y(p1)，

其中，y(pi)代表點(diǎn)pi的y值.使用SMT求解器判斷可行解p2是否存在，得到p2=(3,3)，由ε(φ)可知x和y的取值都達(dá)到了各自的上界，因此，更新最優(yōu)解的最小上界為

UA≡y≤3∧x+y≤6.

4) 將φ∧UA送入SMT求解器，求得可行解為(x=5)∧(y=3)，記為p3=(5,3)，更新最小上界為

UA≡y≤3∧x+y≤8.

5) 提取目標(biāo)函數(shù)H的第2個(gè)元素x+y，在滿(mǎn)足x+y≤∞的基礎(chǔ)上，使用SMT求解器求得優(yōu)于p3的可行解p4=(6,3)，重復(fù)此求解步驟，發(fā)現(xiàn)x+y的值可以無(wú)限的增大，求解過(guò)程無(wú)法終止，判定此最優(yōu)解為無(wú)窮大，即x+y是無(wú)上界的，因此，更新最優(yōu)解的最小上界為

UA≡y≤3，

此時(shí)，UA≡O(shè)A，求解結(jié)束，得到最優(yōu)解為

optT(φ)≡y≤3.

因此，xopt=∞∧yopt≤3.

4.5.3 SMT在線(xiàn)性約束優(yōu)化問(wèn)題求解中的應(yīng)用

Sebastiani等人[11]提出了求解線(xiàn)性實(shí)數(shù)算術(shù)問(wèn)題全局最優(yōu)解的方法，主要思想是通過(guò)可行解測(cè)試(feasibility test)、查找關(guān)鍵點(diǎn)(critical finding)、全局檢查(global checking)三個(gè)步驟來(lái)找到全局最優(yōu)解.在可行解測(cè)試中，算法利用SMT求解器求出符合約束條件的可行解，然后在這些可行解中找出局部最優(yōu)解作為全局最優(yōu)解的候選解.在全局檢查步驟中，算法利用SMT求解器MathSAT對(duì)每個(gè)候選解進(jìn)行測(cè)試，檢查其是否為最優(yōu)解.該算法被集成到基于SMT的優(yōu)化求解器OPT-MathSAT中.

Li等人[111]研發(fā)的SYMBA求解器也可以獲取線(xiàn)性實(shí)數(shù)算術(shù)問(wèn)題的全局最優(yōu)解，求解步驟主要分為全局推送(GLOBALPUSH)和檢測(cè)是否無(wú)界(UNBOUNDED)2個(gè)階段.在GLOBALPUSH階段，SYMBA使用Z3判斷是否存在1個(gè)新的可行解優(yōu)于當(dāng)前最優(yōu)解，如果存在，調(diào)整當(dāng)前最優(yōu)解的最小下界，如果不存在，則說(shuō)明當(dāng)前最優(yōu)解即為全局最優(yōu)解.在UNBOUNDED階段，SYMBA會(huì)檢測(cè)當(dāng)前最優(yōu)解是否無(wú)界，并調(diào)整其最大上界和最小上界.SYMBA會(huì)重復(fù)這2個(gè)階段直至找到全局最優(yōu)解為止.

微軟研發(fā)的νZ[112]可以求解基于SMT公式的線(xiàn)性?xún)?yōu)化問(wèn)題.νZ求解線(xiàn)性實(shí)數(shù)算術(shù)問(wèn)題的方法與OPT-MathSAT的方法類(lèi)似，區(qū)別在于νZ使用SMT求解器MaxSMT求解約束可滿(mǎn)足性問(wèn)題(constraint-satisfaction problem)并利用OptSMT模塊優(yōu)化線(xiàn)性算數(shù)目標(biāo)函數(shù).微軟在Z3中也實(shí)現(xiàn)了相同的功能.

4.6 基于SMT的其他應(yīng)用

Arkoudas等人[19]提出了一種訪(fǎng)問(wèn)控制策略自動(dòng)分析方法.該方法使用可編程定理證明系統(tǒng)Athena實(shí)現(xiàn)了策略的框架表示，并把策略轉(zhuǎn)化為SMT公式，調(diào)用Athena中的SMT求解接口smt-solve求解公式的可滿(mǎn)足性，再對(duì)策略進(jìn)行分析.

Malozemoff等人[113]提出了一種分組密碼加密安全性的自動(dòng)分析與檢測(cè)方法，該方法首先將加密步驟抽象為含有不同種類(lèi)節(jié)點(diǎn)的有向無(wú)環(huán)圖，圖中不同節(jié)點(diǎn)代表不同的操作，邊代表節(jié)點(diǎn)的輸入或輸出.需要將圖中的點(diǎn)和邊轉(zhuǎn)化為約束可滿(mǎn)足性問(wèn)題并使用Z3求解問(wèn)題的可滿(mǎn)足性，根據(jù)結(jié)果判斷模式(mode)是有效的(valid)、解密的(decryptable)還是安全的(secure).

李舟軍等人[114]對(duì)安全漏洞檢測(cè)技術(shù)進(jìn)行了較為全面的總結(jié)，并且介紹了SMT在自動(dòng)化白盒模糊測(cè)試中的應(yīng)用：首先利用文中提出的輕量級(jí)動(dòng)態(tài)符號(hào)執(zhí)行方法獲取程序的執(zhí)行路徑，再借助SMT求解器對(duì)路徑約束求解，用于檢測(cè)程序的漏洞.

5 結(jié)論與展望

SMT以其豐富的背景理論和高效的組合背景理論求解技術(shù)成為了可滿(mǎn)足性問(wèn)題求解領(lǐng)域的核心.SMT求解器可以求解含有組合背景理論的一階邏輯公式，直接處理一些含有高層級(jí)信息的可滿(mǎn)足問(wèn)題，成為了許多實(shí)際應(yīng)用的基礎(chǔ).

本文力圖詳盡地介紹SMT原理、求解方法、工具及最新的應(yīng)用進(jìn)展.詳細(xì)地闡述了SAT，SMT判定算法及理論組合判定算法的實(shí)現(xiàn).根據(jù)近11年SMT-COMP競(jìng)賽的結(jié)果，比較了能夠處理大規(guī)模工業(yè)化應(yīng)用問(wèn)題的主流SMT求解器的綜合求解能力.從應(yīng)用的角度闡述了SMT在測(cè)試用例自動(dòng)生成、程序缺陷檢測(cè)、RTL驗(yàn)證、程序分析與驗(yàn)證以及線(xiàn)性邏輯約束公式優(yōu)化問(wèn)題求解等領(lǐng)域中的具體應(yīng)用.

對(duì)于SMT在各個(gè)領(lǐng)域中的實(shí)際應(yīng)用而言，還存在著許多新的研究熱點(diǎn)和難點(diǎn).例如，基于有界模型檢測(cè)的程序缺陷檢測(cè)受限于界限K，如果想證明程序不違反安全屬性要確保：1)程序在界限K內(nèi)不違反安全屬性;2)程序中循環(huán)的次數(shù)≤K，那么如何驗(yàn)證循環(huán)次數(shù)遠(yuǎn)大于K的程序正確性是1個(gè)新的研究熱點(diǎn).

基于SAT的門(mén)級(jí)電路驗(yàn)證會(huì)產(chǎn)生狀態(tài)爆炸問(wèn)題，將SMT與RTL驗(yàn)證相結(jié)合可以很好地緩解這個(gè)問(wèn)題，因此許多學(xué)者對(duì)此做了相關(guān)的研究[10,101]，但如何利用SMT驗(yàn)證RTL電路的完全正確性也是未來(lái)研究的難點(diǎn).

對(duì)于SMT求解器本身而言，大多數(shù)SMT求解器只接受無(wú)量詞一階邏輯公式作為輸入，實(shí)際問(wèn)題中經(jīng)常會(huì)含有全稱(chēng)量詞(?)，求解此類(lèi)問(wèn)題是目前SMT求解器的難點(diǎn)之一，僅有少數(shù)幾個(gè)主流的SMT求解器支持帶有全稱(chēng)量詞問(wèn)題的求解，比如Z3，CVC4等.求解方法主要分為2種：1)基于模式(pattern-based)的量詞實(shí)例化方法，主要是將帶有全稱(chēng)量詞的變量實(shí)例化為帶有存在量詞(?)的變量，比如將(?x,x>1)實(shí)例化為(?x=2,x>1).但是如何選取x的具體實(shí)例化數(shù)值是有待研究的問(wèn)題.2)基于飽和定理證明(saturation theorem proving)，此方法使用了疊加演算的思想解決公式中的量詞問(wèn)題.含有全稱(chēng)量詞的一階邏輯公式可滿(mǎn)足性求解算法將是今后的研究熱點(diǎn).

[1]Johnson K, Calinescu R. Efficient re-resolution of SMT specifications for evolving software architectures[C]Proc of the 10th Int ACM Sigsoft Conf on Quality of Software Architectures. New York: ACM, 2014: 93-102

[2]Malik S U R, Khan S U, Srinivasan S K. Modeling and analysis of state-of-the-art VM-based cloud management platforms[J]. IEEE Trans on Cloud Computing, 2013, 1(1): 50-63

[3]Cotrini C, Weghorn T, Basin D, et al. Analyzing first-order role based access control[C]Proc of the 28th IEEE Computer Security Foundations Symp. Piscataway, NJ: IEEE, 2015: 3-17

[4]Arkoudas K, Chadha R, Chiang J. Sophisticated access control via SMT and logical frameworks[J]. ACM Trans on Information and System Security, 2014, 16(4): 1-31

[5]Voss S, Schatz B. Deployment and scheduling synthesis for mixed-critical shared-memory applications[C]Proc of the 20th IEEE Int Conf and Workshops on the Engineering of Computer Based Systems. Piscataway, NJ: IEEE, 2013: 100-109

[6]Huang Yu, Mercer E, Mccarthy J. Proving MCAPI executions are correct using SMT[C]Proc of the 28th IEEE Int Conf on Automated Software Engineerin. Piscataway, NJ: IEEE, 2013: 26-36

[7]Cordeiro L, Fischer B, Marques-Silva J. SMT-based bounded model checking for embedded ANSI-C software[J]. IEEE Trans on Software Engineering, 2012, 38(4): 957-974

[8]Barnat J, Bauch P, Havel V. Model checking parallel programs with inputs[C]Proc of the 22nd Euromicro Int Conf on Parallel, Distributed and Network-Based Processing(PDP). Piscataway, NJ: IEEE, 2014: 756-759

[9]Liu Leyuan, Kong Werqiang, Ando T, et al. A survey of acceleration techniques for SMT-based bounded model checking[C]Proc of 2013 Int Conf on Computer Sciences and Applications (CSA). Piscataway, NJ: IEEE, 2013: 554-559

[10]Kunapareddy S, Turaga S D, Sajjan S S T M. Comparision between LPSAT and SMT for RTL verification[C]Proc of Int Conf on Circuit, Power and Computing Technologies. Piscataway, NJ: IEEE, 2015

[11]Sebastiani R, Tomasi S. Optimization in SMT with LA()cost functions[G]LNAI 7364: Automated Reasoning. Berlin: Springer, 2012: 484-498

[12]Chen Li, Wang Yongji, Wu Jingzheng, et al. Rate-Monotonic optimal design based on tree-like linear programming search[J]. Journal of Software, 2015, 26(12): 3223-3241 (in Chinese)(陳力, 王永吉, 吳敬征, 等. 基于樹(shù)狀線(xiàn)性規(guī)劃搜索的單調(diào)速率優(yōu)化設(shè)計(jì)[J]. 軟件學(xué)報(bào), 2015, 26(12): 3223-3241)

[13]Blackham B, Liffiton M, Heiser G. Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets[C]Proc of Real-Time and Embedded Technology and Applications Symp. Piscataway, NJ: IEEE, 2014: 169-178

[14]Eldib H, Wang Chao, Taha M, et al. Quantitative masking strength: Quantifying the power side-channel resistance of software code[J]. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 2015, 34(10): 1558-1568

[15]Leroy X . Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115

[16]Klein G. Operating system verification—An overview[J]. Sadhana, 2009, 34(1): 27-69

[17]Cook S A. The complexity of theorem-proving procedures[C]Proc of the 3rd Annual ACM Symp on Theory of Computing. New York: ACM, 1971: 151-158

[18]Cousot P, Cousot R, Feret J, et al. The ASTRéE analyzer[G]LNCS 3444: Programming Languages and Systems. Berlin, Springer, 2005: 21-30

[19]Arkoudas K, Loeb S, Chadha R, et al. Automated policy analysis[C]Proc of 2012 IEEE Int Symp on Policies for Distributed Systems and Networks(POLICY). Piscataway, NJ: IEEE, 2012

[20]Nuzzo P, Puggelli A, Seshia S A, et al. CalCS: SMT solving for non-linear convex constraints[C]Proc of the 2010 Conf on Formal Methods in Computer-Aided Design. Piscataway, NJ: IEEE, 2010: 71-80

[21]Chimisliu V, Wotawa F. Category partition method and satisfiability modulo theories for test case generation[C]Proc of the 7th Int Workshop on Automation of Software Test Piscataway, NJ: IEEE, 2012: 64-70

[22]Riener H, Bloem R, Fey G. Test case generation from mutants using model checking techniques[C]Proc of the 4th IEEE Int Conf on Software Testing, Verification and Validation Workshops (ICSTW). Piscataway, NJ: IEEE, 2011: 388-397

[23]Jo?Bstl E, Weiglhofer M, Aichernig B K, et al. When bdds fail: Conformance testing with symbolic execution and SMT solving[C]Proc of the 3rd Int Conf on Software Testing, Verification and Validation(ICST). Piscataway, NJ: IEEE, 2010: 479-488

[24]Ansótegui C, Bofill M, Manyà F, et al. Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers[C]Proc of the 42nd IEEE Int Symp on Multiple-Valued Logic(ISMVL). Piscataway, NJ: IEEE, 2012: 25-30

[25]Shostak R E. An algorithm for reasoning about equality[J]. Communications of the ACM, 1978, 21(2): 583-585

[26]Shostak R E. Deciding combinations of theories[J]. Journal of the ACM, 1984, 31(1): 209-222

[27]Shostak R E. A practical decision procedure for arithmetic with function symbols[J]. Journal of the ACM, 1979, 26(2): 351-360

[28]Armando A, Giunchiglia E. Embedding complex decision procedures inside an interactive theorem prover[J]. Annals of Mathematics & Artificial Intelligence, 1993, 8(34): 475-502

[29]Armando A, Castellini C, Giunchiglia E. SAT-based procedures for temporal reasoning[G]LNAI 1809: Proc of the 5th European Conf on Planning: Recent Advances in AI Planning. Berlin: Springer, 2000: 97-108

[30]Bryant R E, German S, Velev M N. Exploiting positive equality in a logic of equality with uninterpreted Functions[C]Proc of the 11th Int Conf on Computer Aided Verification. Berlin: Springer, 1999: 470-482

[31]Giunchiglia F, Sebastiani R . Building decision procedures for modal logics from propositional decision procedures: The case study of modalK(m)[J]. Information & Computation, 2000, 162(1): 158-178

[32]Zhang Jian. Specification analysis and test data generation by solving Boolean combinations of numeric constraints[C]Proc of the 1st Asia-Pacific Conf on Quality Software. Piscataway, NJ: IEEE, 2000: 267-274

[33]Malik S, Zhang Lintao. Boolean satisfiability from theoretical hardness to practical success[J]. Communications of the ACM, 2009, 52(8): 76-82

[34]De Moura L, Bj?rner N. Z3: An efficient SMT solver[G]LNCS 4936: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008: 337-340

[35]Barrett C, Deters M, Conway C L, et al. CVC4[G]LNCS 6806: Proc of the 23rd Int Conf on Computer Aided Verification. Berlin: Springer, 2011: 171-177

[36]Dutertre B. Yices2.2[G]LNCS 8559: Proc of the 16th Int Conf on Computer Aided Verification. Berlin: Springer, 2014: 737-744

[37]Bruttomesso R, Cimatti A, Franzén A, et al. The mathsat4 smt solver[G]LNCS 5123: Proc of the 20th Int Conf on Computer Aided Verification. Berlin: Springer, 2008: 299-303

[38]Brummayer R, Biere A. Boolector: An efficient SMT solver for bit-vectors and arrays[G]LNCS 5505: Proc of Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2009: 174-177

[39]Godefroid P, De Halleux P, Nori A V, et al. Automating software testing using program analysis[J]. IEEE Software, 2008, 25(5): 30-37

[40]Henzinger T A, Jhala R, Majumdar R, et al. Lazy abstraction[J]. ACM SIGPLAN Notices, 2002, 37(1): 58-70

[41]Wang Jianxin, Guan Lina, Jiang Guohong. A survey of algorithms for SAT problem[J]. Computing Technology and Automation, 2009, 28(4): 138-143 (in Chinese)(王建新, 管利娜, 江國(guó)紅. 可滿(mǎn)足性問(wèn)題的研究綜述[J]. 計(jì)算技術(shù)與自動(dòng)化, 2009, 28(4): 138-143)

[42]Sheini H M, Sakallah K A. From propositional satisfiability to satisfiability modulo theories[G]LNCS 4121: Proc of the 9th Int Conf Seattle. Berlin: Springer, 2006

[43]Moura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo yheories[G]LNCS 4590: Proc of the 19th Int Conf on Computer Aided Verification. Berlin: Springer, 2007: 20-36

[44]Jin Jiwei, Ma Feifei, Zhang Jian. Brief introduction to SMT solving[J]. Journal of Frontiers of Computer Science & Technology, 2015, 9(7): 769-780 (in Chinese)(金繼偉, 馬菲菲, 張健. SMT求解技術(shù)簡(jiǎn)述[J]. 計(jì)算機(jī)科學(xué)與探索, 2015, 9(7): 769-780)

[45]Singer D. Parallel Resolution of the Satisfiability Problem: A Survey[M]. New York: John Wiley & Sons, 2006: 123-148

[46]Hansen P, Jaumard B. Algorithms for the maximum satisfiability problem[J]. Computing, 1990, 44(4): 279-303

[47]Bistarelli S, Montanari U, Rossi F, et al. Semiring-based CSPs and valued CSPs: Frameworks, properties, and comparison[J]. Constraints, 1999, 4(3): 199-240

[48]Mahajan M, Raman V. Parameterizing above guaranteed values: Maxsat and maxcut[J]. Journal of Algorithms, 1999, 31(2): 335-354

[49]Davis M, Putnam H. A computing procedure for quantification theory[J]. Journal of the ACM, 1960, 7(3): 201-215

[50]Davis M, Logemann G, Loveland D. A machine program for theorem-proving[J]. Communications of the ACM, 1962, 5(7): 394-397

[51]Prestwich S. Lynce I: Local search for unsatisfiability[G]LNCS 4121: Proc of Theory and Applications of Satisfiability Testing-SAT 2006. Berlin: Springer, 2006: 283-296

[52]Audemard G, Simon L. GUNSAT: A greedy local search algorithm for unsatisfiability[C]Proc of 2007 Int Joint Conf on Artificial Intelligence. San Francisco: Morgan Kaufmann, 2007: 2256-2261

[53]Xu Daoyun Liu Changyun. DPLL algorithm with literal renaming strategy[J]. Journal of Frontiers of Computer Science & Technology, 2007, 1(1): 116-125 (in Chinese)(許道云, 劉長(zhǎng)云. 帶文字改名策略的 DPLL 算法[J]. 計(jì)算機(jī)科學(xué)與探索, 2007, 1(1): 116-125)

[54]Nieuwenhuis R, Oliveras A, Rodríguez-Carbonell E, et al. Challenges in satisfiability modulo theories[G]LNCS 4533: Proc of Term Rewriting and Applications. Berlin: Springer, 2007: 2-18

[55]Barrett C, Stump A, Tinelli C. The satisfiability modulo theories library (smt-lib)[EBOL]. 2010[2016-04-03]. http:www.SMT-LIB.org

[56]Mccarthy J. Towards a Mathematical Science of Computation[M]. Berlin: Springer, 1993: 35-56

[57]Barrett C, Tinelli C. Cvc3[G]LNCS 4590: Proc of the 19th Int Conf on Computer Aided Verification. Berlin: Springer, 2007: 298-302

[58]Nelson G, Oppen D C. Simplification by cooperating decision procedures[J]. ACM Trans on Programming Language System, 1979, 1(2): 245-257

[59]Bozzano M, Bruttomesso R, Cimatti A, et al. Efficient satisfiability modulo theories via delayed theory combination[G]LNCS 3676: Proc of Computer Aided Verification. Berlin: Springer, 2005: 335-349

[60]Nelson G, Oppen D C. Fast decision procedures based on congruence closure[J]. Journal of the ACM, 1980, 27(2): 356-364

[61]Huang Zhuo, Zhang Jian. Generating SAT instances from first-order formulas[J]. Journal of Software, 2005, 16(3): 327-335

[62]Seshia S A, Lahiri S K, Bryant R E. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions[C]Proc of the 40th Annual Design Automation Conf. New York: ACM, 2003: 425-430

[63]Bryant R E, Lahiri S K, Seshia S A. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions[G]LNCS 2404: Proc of the 2002 Int Conf on Computer Aided Verification. Berlin: Springer, 2002: 78-92

[64]Pnueli A, Rodeh Y, Shtrichman O, et al. Deciding equality formulas by small domains instantiations[G]LNCS 1633: Proc of the 1999 Int Conf on Computer Aided Verification. Berlin: Springer, 1999: 455-469

[65]Talupur M, Sinha N, Strichman O, et al. Range allocation for separation logic[G]LNCS 3114: Proc of the 2004 Int Conf on Computer Aided Verification. Berlin: Springer, 2004: 148-161

[66]Goel A, Sajid K, Zhou H, et al. BDD based procedures for a theory of equality with uninterpreted functions[C]Proc of the 1998 Int Conf on Computer Aided Verification. Berlin: Springer, 1998: 244-255

[67]Barrett C W, Dill D L, Stump A. Checking satisfiability of first-order formulas by incremental translation to SAT[C]Proc of the 2002 Int Conf on Computer Aided Verification. Berlin: Springer, 2002: 236-249

[68]Wolfman S A, Weld D S. The LPSAT engine & its application to resource planning[C]Proc of the 16th Int Joint Conf on Artificial Intelligence. San Francisco: Morgan Kaufmann, 1999: 310-317

[69]Ball T, Cook B, Lahiri S K, et al. Zapato: Automatic theorem proving for predicate abstraction refinement[G]LNCS 3114: Proc of Computer Aided Verification. Berlin: Springer, 2004: 457-461

[70]Bruno D, Leonardo D M. A fast linear-arithmetic solver for DPLL(T)[G]LNCS 4144: Proc of Computer Aided Verification. Berlin: Springer, 2006: 81-94

[71]Ganzinger H, Hagen G, Nieuwenhuis R, et al. DPLL(T): Fast decision procedures[G]LNCS 3114: Proc of Computer Aided Verification. Berlin: Springer, 2004: 175-188

[72]Bozzano M, Bruttomesso R, Cimatti A, et al. Efficient theory combination via Boolean search[J]. Information and Computation, 2006, 204(10): 1493-1525

[73]Sebastiani R. Lazy satisfiability modulo theories[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2007, 3(9): 141-224

[74]Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories: From an abstract davis-putnam-logemann-loveland procedure to DPLL (T)[J]. Journal of the ACM, 2006, 53(6): 937-977

[75]Flanagan C, Joshi R, Ou X, et al. Theorem proving using lazy proof explication[G]LNCS 2725: Proc of Computer Aided Verification. Berlin: Springer, 2003: 355-367

[76]Bozzano M, Bruttomesso R, Cimatti A, et al. An incremental and layered procedure for the satisfiability of linear arithmetic logic[G]LNCS 3440: Proc of Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2005: 317-333

[77]Jha S, Limaye R, Seshia S A. Beaver: Engineering an efficient smt solver for bit-vector arithmetic[G]LNCS 5643: Proc of Computer Aided Verification. Berlin: Springer, 2009: 668-674

[78]Armando A, Castellini C, Giunchiglia E, et al. A SAT-based decision procedure for the Boolean combination of difference constraints[G]LNCS 3542: Proc of Theory and Applications of Satisfiability Testing. Berlin: Springer, 2005: 16-29

[79]Bofill M, Nieuwenhuis R, Oliveras A, et al. The barcelogic SMT solver[G]LNCS 5123: Proc of the 20th Int Conf on Computer Aided Verification. Berlin: Springer, 2008: 294-298

[80]Bouton T, De Oliveira D C B, Déharbe D, et al. VeriT: An open, trustable and efficient SMT-solver[G]LNAI 5663: Proc of 2009 Int Conf on Automated Deduction. Berlin: Springer, 2009: 151-156

[81]Lahiri S, Qadeer S. Back to the future: Revisiting precise program verification using SMT solvers[J]. ACM SIGPLAN Notices, 2008, 43(1): 171-182

[82]Gulavani B S, Henzinger T A, Kannan Y, et al. SYNERGY: A new algorithm for property checking[C]Proc of the 14th ACM SIGSOFT Int Symp on Foundations of Software Engineering. New York: ACM, 2006: 117-127

[83]Ball T, Rajamani S K. The SLAM project: Debugging system software via static analysis[C]Proc of ACM SIGPLAN Notices. New York: ACM, 2002: 1-3

[84]Costa M, Crowcroft J, Castro M, et al. Vigilante: End-to-end containment of internet worms[C]Proc of 2005 ACM SIGOPS Operating Systems Review. New York: ACM, 2005: 133-147

[85]Godefroid P, Levin M Y, Molnar D. SAGE: Whitebox fuzzing for security testing[J]. Communications of the ACM, 2012, 55(3): 40-44

[86]Anand S, P?s?reanu C S, Visser W. JPF-SE: A symbolic execution extension to Java pathfinder[G]LNCS 4424: Proc of Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2007: 134-138

[87]Arcaini P, Gargantini A, Vavassori P. Generating tests for detecting faults in feature models[C]Proc of the 8th IEEE Int Conf on Software Testing, Verification and Validation. Piscataway, NJ: IEEE, 2015

[88]Lin Huimin, Zhang Wenhui. Model checking: Theories, technigues and applications[J]. Acta Electronica Sinica, 2002, 30(12): 1907-1912 (in Chinese)(林惠民, 張文輝. 模型檢測(cè): 理論, 方法與應(yīng)用[J]. 電子學(xué)報(bào), 2002, 30(12): 1907-1912)

[89]Ramalho M, Freitas M, Sousa F, et al. SMT-based bounded model checking of C++ programs[C]Proc of the 20th IEEE Int Conf and Workshops on Engineering of Computer Based Systems(ECBS). Piscataway, NJ: IEEE, 2013: 147-156

[90]Cordeiro L. SMT-based bounded model checking of multi-threaded software in embedded systems[C]Proc of the 32nd ACMIEEE Int Conf on Software Engineering. Piscataway, NJ: IEEE, 2011: 373-376

[91]Cordeiro L, Fischer B. Verifying multi-threaded software using smt-based context-bounded model checking[C]Proc of the 33rd Int Conf on Software Engineering. Piscataway, NJ: IEEE, 2011: 331-340

[92]Mueller F. A library implementation of POSIX threads under UNIX[C]Proc of the USENIX Conf. Berkeley, CA: USENIX Association, 1993: 29-42

[93]Pereira P A, Albuquerque H F, Marques H M, et al. Verifying CUDA programs using SMT-based context-bounded model checking[EBOL]. [2016-04-02]. http:svlab.hussamaismail.eti.brpaperssac2016.pdf

[94]Cheng J, Grossman M, Mckercher T. Professional Cuda C Programming[M]. New York: John Wiley & Sons, 2014

[95]Morse J. Expressive and efficient bounded model checking of concurrent software[D]. Southampton: University of Southampton, 2015

[96]Ball T, Rajamani S K. Automatically validating temporal safety properties of interfaces[G]LNCS 2057: Proc of the 8th Int SPIN Workshop on Model Checking of Software. Berlin: Springer, 2001: 103-122

[97]Lingappan L, Ravi S, Jha N K. Satisfiability-based test generation for nonseparable RTL controller-datapath circuits[J]. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 2006, 25(3): 544-557

[98]Duraira V, Kalla P. Exploiting hypergraph partitioning for efficient Boolean satisfiability[C]Proc of the 9th IEEE Int High-Level Design Validation and Test Workshop. Piscataway, NJ: IEEE, 2004: 141-146

[99]Kroening D, Seshia S A. Formal verification at higher levels of abstraction[C]Proc of IEEEACM Int Conf on Computer -Aided Design. Piscataway, NJ: IEEE, 2007: 572-578

[100]Clarke E, Grumberg O, Jha S, et al. Counterexample-guided abstraction refinement[G]LNCS 1855: Proc of Computer Aided Verification. Berlin: Springer, 2000: 154-169

[101]Puri P, Bradley M S H. SI-SMART: Functional test generation for RTL circuits using loop abstraction and learning recurrence relationships[C]Proc of the 33rd IEEE Int Conf on Computer Design. Piscataway, NJ: IEEE, 2015: 38-45

[102]Brady B, Bryant R E, Seshia S, et al. ATLAS: Automatic term-level abstraction of RTL designs[C]Proc of the 8th IEEEACM Int Conf on Formal Methods and Models for Codesign. Piscataway, NJ: IEEE, 2010: 31-40

[103]Zhao Yanni, Bian Jinian, Deng Shujun. Constraints decomposition for RTL verification by SMT[J]. Journal of Computer-Aided Design & Computer Graphics, 2010, 22(2): 234-239 (in Chinese)(趙燕妮, 邊計(jì)年, 鄧澍軍. 利用 SMT 約束分解方法求解 RTL 可滿(mǎn)足性問(wèn)題[J]. 計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào), 2010, 22(2): 234-239)

[104]Gent K, Hsiao M S. Functional test generation at the RTL using swarm intelligence and bounded model checking[C]Proc of the 22nd Asian Test Symp. Piscataway, NJ: IEEE, 2013: 233-238

[105]Liu L, Vasudevan S. Efficient validation input generation in RTL by hybridized source code analysis[C]Proc of Design, Automation and Test in Europe Conf & Exhibition. Piscataway, NJ: IEEE, 2011

[106]He Yanxiang, Wu Wei, Chen Yong, et al. Path sensitive program verification based on SMT solvers[J]. Journal of Software, 2012, 23(10): 2655-2664 (in Chinese)(何炎祥, 吳偉, 陳勇, 等. 基于SMT求解器的路徑敏感程序驗(yàn)證[J]. 軟件學(xué)報(bào), 2012, 23(10): 2655-2664)

[107]Paganelli G, Ahrendt W. Verifying (in-)stability in floating-point programs by increasing precision, using SMT solving[C]Proc of the 15th Int Symp on Symbolic and Numeric Algorithms for Scientific Computing. Piscataway, NJ: IEEE, 2013: 209-216

[108]Kroening D, Weissenbacher G. Interpolation-based software berification with WOLVERINE[G]LNCS 6806: Proc of the 23rd Int Conf on Computer Aided Verification. Berlin: Springer, 2011: 573-578

[109]Pigorsch F, Scholl C. Lemma localization: A practical method for downsizing SMT-interpolants[C]Proc of the Conf on Design, Automation and Test in Europe. San Jose, CA: EDA Consortium, 2013: 1405-1410

[110]Cohen E, Dahlweid M, Hillebrand M, et al. VCC: A practical system for verifying concurrent C[G]LNCS 5674: Proc of Theorem Proving in Higher Order Logics. Berlin: Springer, 2009: 23-42

[111]Li Yi, Albarghouthi A, Kincaid Z, et al. Symbolic optimization with SMT solvers[C]Proc of the 41st ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages. New York: ACM, 2014: 607-618

[112]Bj?rner N, Phan A-D, Fleckenstein L. νZ-an optimizing SMT solver[G]LNCS 9035: Proc of Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2015: 194-199

[113]Malozemoff A J, Katz J, Green M D. Automated analysis and synthesis of block-cipher modes of operation[C]Proc of the 27th IEEE Computer Security Foundations Symp. Piscataway, NJ: IEEE, 2014: 140-152

[114]Li Zhoujun, Zhang Junxian, Liao Xiangke, et al. Survey of software vulnerability detection techniques[J]. Chinese Journal of Computers, 2015, 38(4): 717-732 (in Chinese)(李舟軍, 張俊賢, 廖湘科, 等. 軟件安全漏洞檢測(cè)技術(shù)[J]. 計(jì)算機(jī)學(xué)報(bào), 2015, 38(4): 717-732)

Wang Chong, born in 1991. PhD candidate. Student member of CCF. His main research interests include satisfiability modulo theories, multicore scheduling algorithm, bounded model checking.

Lü Yinrun, born in 1991. PhD candidate. His main research interests include satisfiability modulo theories, optimization algorithm.

Chen Li, born in 1989. PhD candidate. His main research interests include satisfiability modulo theories, real-time system, optimization algorithm.

Wang Xiuli, born in 1997. Associate professor and PhD supervisor. His main research interests include information security and game theory.

Wang Yongji, born in 1962. Professor and PhD supervisor. Senior member of CCF. He is the winner of the 2002 One-Hundred-Talent People Program sponsored by the Chinese Academy of Sciences. His main research interests include computer-controlled real-time systems, network optimization theory, intelligent software engineering, nonlinear optimization theory, real-time hybrid control theory, real-time embedded operating system, etc.

Survey on Development of Solving Methods and State-of-the-Art Applications of Satisfiability Modulo Theories

Wang Chong1,2,3, Lü Yinrun1,2,3, Chen Li1,2,3, Wang Xiuli4, and Wang Yongji1,3

1(NationalEngineeringResearchCenterforFundamentalSoftware(InstituteofSoftware,ChineseAcademyofSciences),Beijing100190)2(UniversityofChineseAcademyofSciences,Beijing100049)3(StateKeyLaboratoryofComputerScience(InstituteofSoftware,ChineseAcademyofSciences),Beijing100190)4(SchoolofInformation,CentralUniversityofFinanceandEconomics,Beijing100081)

The satisfiability modulo theories (SMT) problem is a decision problem for the satisfiability of first-order logical formula with respect to combinations of background theories. SMT supports many background theories, so it can describe a lot of practical problems in industrial fields or academic circles. Also, the expression ability and the efficiency of decision algorithms of SMT are both better than those of SAT (satisfiability). With its efficient satisfiability decision algorithms, SMT has been widely used in many fields, in particular in test-case generation, program defect detection, register transfer level (RTL) verification, program analysis and verification, solving linear optimization over arithmetic constraint formula, etc. In this paper, we firstly summarize fundamental problems and decision procedures of SAT. After that, we give a brief overview of SMT, including its fundamental concepts and decision algorithms. Then we detail different types of decision algorithms, including eager and lazy algorithms which have been studied in the past five years. Moreover, some state-of-the-art SMT solvers, including Z3, Yices2 and CVC4 are analyzed and compared based on the results of the SMT’s competition. Additionally, we also focus on the introduction for the application of SMT solving in some typical communities. At last, we give a preliminary prospect on the research focus and the research trends of SMT.

satisfiability modulo theories (SMT); SMT solver; decision algorithms of SMT; test-case generation; program defect detection; cloud computing

2016-04-26；

2016-07-14

國(guó)家自然科學(xué)基金項(xiàng)目(61170072，61303057)；中國(guó)科學(xué)院、國(guó)家外國(guó)專(zhuān)家局創(chuàng)新團(tuán)隊(duì)國(guó)際合作伙伴計(jì)劃 This work was supported by the National Natural Science Foundation of China (61170072,61303057) and the CASSAFEA International Partnership Program for Creative Research Teams.

王永吉(ywang@itechs.iscas.ac.cn)

TP301