王 翀 呂蔭潤 陳 力 王秀利 王永吉

1(基礎(chǔ)軟件國家工程研究中心(中國科學(xué)院軟件研究所) 北京 100190)2(中國科學(xué)院大學(xué) 北京 100049)3(計算機科學(xué)國家重點實驗室(中國科學(xué)院軟件研究所) 北京 100190)4 (中央財經(jīng)大學(xué)信息學(xué)院 北京 100081)

?

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

王 翀1,2,3呂蔭潤1,2,3陳 力1,2,3王秀利4王永吉1,3

1(基礎(chǔ)軟件國家工程研究中心(中國科學(xué)院軟件研究所) 北京 100190)2(中國科學(xué)院大學(xué) 北京 100049)3(計算機科學(xué)國家重點實驗室(中國科學(xué)院軟件研究所) 北京 100190)4(中央財經(jīng)大學(xué)信息學(xué)院 北京 100081)

(wangchong@nfs.iscas.ac.cn)

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

可滿足性模理論；SMT求解器；SMT求解算法；測試用例自動生成；程序缺陷檢測；云計算

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

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

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

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

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

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

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

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

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

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

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

1 SAT問題及判定算法

1.1 SAT問題

SAT問題是命題邏輯公式(propositional logical formula)的可滿足性判定問題，下面先介紹有關(guān)命題邏輯的一些必要概念.命題邏輯中的邏輯運算符號(又稱二元連接符)是指定義在布爾集合上的邏輯運算，包括∧(與)，∨(或)，(非)，→(蘊含)，?(等價)，⊕(異或).命題變元的取值為真或為假，在取值意義上等價為布爾變量.命題邏輯公式的形成規(guī)則為

1) 命題邏輯公式f(或SAT公式f)可以是單獨的命題變元，也稱為原子公式;

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

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

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

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

1.2 SAT問題判定算法

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

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

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

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

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

decide通過一些策略來選取1個尚未賦值的變量，并將它的值指定為真或假.

fail用于檢測公式f在當前搜索空間下的可滿足性以及是否存在沖突.

backtrack在fail檢測到公式f在當前搜索空間不可滿足時進行回溯，返回到上1層搜索空間并通過decide重新尋找賦值變量.

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

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

2) 使用decide操作對f中1個未賦值的變量進行賦值；

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

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

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

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

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

現(xiàn)代DPLL搜索算法均是在此基礎(chǔ)上進行改進的，典型的基于沖突檢測的子句學(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ū)別在于每當UnitPropagation執(zhí)行完成后，ConflictDetetction便會檢測是否存在沖突，若存在沖突，則調(diào)用ConflicAnalysis分析沖突產(chǎn)生的原因并進行子句學(xué)習(xí)，以此確定回溯的層次.

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

2 SMT問題及判定算法

2.1 SMT問題及背景理論

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

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

SMT-LIB[55]是公認程度較高的SMT研究標準，主要包括：

1) 規(guī)定了SMT求解器標準輸入輸出的語言規(guī)范；

2) 建立了格式嚴格統(tǒng)一的背景理論知識測試集，用來評價和比較SMT求解器的求解能力；

3) 提出了SMT背景理論的規(guī)范，主要分為未解釋函數(shù)理論(quantifier free_uninterpreted function, QF_UF)、數(shù)組理論(quantifier free_arrays, QF_AQF_AX)、整數(shù)集實數(shù)集上的線性算數(shù)理論(quantifier free_linear integer arithmeticquantifier free_linear real arithmetic, QF_LIAQF_LRA)、整數(shù)集實數(shù)集上的非線性算數(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ù)差分邏輯理論(quantifier free_difference logic over the reals, QF_RDL)、位向量理論(QF_BV)等.

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

規(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)系需要通過未解釋函數(shù)理論進行定義，例如(array=array′∧i=j)被等價地定義為(select(array,i)=select(array′,j)).基于QF-UF可以對數(shù)組背景理論可以進行如下擴展：

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

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

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

x1-x2⊙J，

(1)

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

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

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中)，⊙∈{=,≥,≤,≠}.

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

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

一些主流SMT求解器(比如Z3，CVC3，Boolector)對線性、非線性、位向量等背景理論的描述為[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代表布爾值表達式，由A和L組成，代表邏輯運算符非.con是邏輯連接符，包括合取(∧)、析取(∨)、蘊含(→)、等價(?)、異或(⊕).B代表由整數(shù)、實數(shù)、位向量構(gòu)成的項，～代表補運算，Const表示常量，Id表示變量.ite(cb,t1,t2)表示if-then-else，如果布爾表達式cb的值為真，則執(zhí)行t1，否則執(zhí)行t2.Extract(B,i,j)表示抽取位向量B的第i到第j位，產(chǎn)生1個新的長度為i-j+1的位向量.SignExt(B,k)表示用k個0擴展位向量B，形成新的長度增加了k位的帶符號位向量.ZeroExt(B,k)跟SignExt(B,k)操作類似，區(qū)別在于ZeroExt(B,k)生成不帶符號的位向量.op代表操作符，包括與(&)、或(|)、四則運算符(+，-，*，)、右移(?)、左移(?)、位向量的級聯(lián)(@).

2.2 組合背景理論求解方法

由實際應(yīng)用問題等價轉(zhuǎn)化而成的SMT問題通常包含多種理論，需要結(jié)合數(shù)組、整數(shù)線性算數(shù)、實數(shù)差分邏輯等多種背景理論才能解釋SMT公式F中每一項的含義，這種情況下單理論判定方法無法滿足判定需求，需要組合理論判定方法的支持，主要方法有：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ǔ)改進而成的.Nelson-Oppen方法的前提是各個背景理論符號集不相交且各理論之間相互獨立，每個背景理論Ti中的無量詞SMT公式都需要有1個可滿足賦值Mi(基于理論的模型).Nelson-Oppen方法首先在各個理論間傳遞含有共享變量的等式，稱為接口等式(interface equation)，然后各個理論將此接口等式加入到自己的約束條件中并進行可滿足性判定.如果出現(xiàn)不可滿足的理論，則此SMT公式是不可滿足的，否則重復(fù)上述步驟直至沒有新的接口等式可以傳遞.如果此時沒有不可滿足的理論，則此SMT公式是可滿足的.Nelson-Oppen方法的缺點是過于依賴于共享變量的傳遞，并且提取共享變量又需要求解器進行純化操作，需要各個背景理論間相互傳遞接口等式.負責(zé)的算法框架使得Nelson-Oppen方法求解效率低下.

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

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

2.3 SMT問題判定算法

2.3.1 求解SMT問題的積極類算法

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

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

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

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

2.3.2 求解SMT問題的惰性算法

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

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

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

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

此算法的優(yōu)勢在于，若算法在步驟2中已判定SAT公式不可滿足，則無需進行后續(xù)判定工作，提高了求解效率.惰性算法是SAT求解器與對應(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是不可滿足的)

return false;

else

for (每個f的模型M)

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

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

return true;

end if

end for

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

return false;

end if

end if

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

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

3 SMT求解器及性能比較

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

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

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

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

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

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

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

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

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

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

在2015年SMT-COMP中，舉辦方提供了40種不同的背景理論測試集，基于每個SMT求解器在各個測試集上的綜合評分，表3給出了主流SMT求解器在不同背景理論測試集中的排名.其中LIA表示整數(shù)線性算數(shù)理論，QF_ABV表示無量詞固定位向量數(shù)組理論，QF_IDL表示無量詞整數(shù)差分邏輯理論，QF_NIA表示無量詞整數(shù)非線性算數(shù)理論，QF_UFLIA表示無量詞未解釋函數(shù)的整數(shù)線性算數(shù)理論，“ ”代表此SMT求解器不支持對應(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求解器的逐漸成熟，人們開始使用SMT解決一些實際問題，例如測試用例自動生成、程序缺陷檢測、RTL驗證、程序分析與驗證、線性邏輯約束公式優(yōu)化問題求解等.

4.1 測試用例自動生成

4.1.1 基于SMT的測試用例自動生成

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

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

2) 當F不可滿足時，說明當前執(zhí)行路徑不正確，修改某一分支語句的分支條件后進行新一輪的路徑構(gòu)造、約束求解.

4.1.2 具體示例

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

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

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

(9)

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

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

(10)

利用SMT求解器判斷出F2是可滿足的，且可滿足解為(choice=1)，達到了測試用例自動生成的目的.

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

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

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

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

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

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

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

4.2 程序缺陷檢測

4.2.1 基于SMT的程序缺陷檢測

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

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

4.2.2 具體示例

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

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

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

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

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

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

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

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

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

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

4.3 RTL驗證

4.3.1 基于SMT的RTL驗證

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

4.3.2 具體示例

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

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

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

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

Kroening等人[99]提出了一種利用高層級信息模型進行RTL驗證的方法，該方法利用謂詞抽象技術(shù)和SMT求解器進行位級以及字級的驗證(word-level verification).結(jié)合了反例指導(dǎo)的抽象框架[100](counterexample guided abstraction refinement frame)的謂詞抽象技術(shù)將系統(tǒng)的實際狀態(tài)空間映射到1個抽象的、狀態(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的自動RTL測試生成器SI-SMART(swarm intelligence-SMART)，目的是解決傳統(tǒng)有界模型檢測方法和基于符號執(zhí)行的檢測方法對循環(huán)處理能力不足的問題.在DUT(design under test)中，循環(huán)是很常見的，但是有界模型檢測或者基于符號執(zhí)行的檢測方法只能將循環(huán)展開至多K次，再進行RTL驗證工作.此方法不適用于DUT.SI-SMART先對DUT中的循環(huán)進行抽象，再找出直接或間接影響目標分支條件的變量，分析它們之間的遞推關(guān)系技術(shù)并以此消除控制流圖中的循環(huán)展開，從而解決了需要按照一定界限展開循環(huán)的問題.

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

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

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

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

4.4 程序分析與驗證

4.4.1 基于SMT的程序分析與驗證

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

4.4.2 具體示例

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

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

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

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

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

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

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

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

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

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

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

4.5.2 具體示例

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

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

(11)

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

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) 將φ中每個原子公式中的不等號替換為等號，得到的集合記為

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

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

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

其中，y(pi)代表點pi的y值.使用SMT求解器判斷可行解p2是否存在，得到p2=(3,3)，由ε(φ)可知x和y的取值都達到了各自的上界，因此，更新最優(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) 提取目標函數(shù)H的第2個元素x+y，在滿足x+y≤∞的基礎(chǔ)上，使用SMT求解器求得優(yōu)于p3的可行解p4=(6,3)，重復(fù)此求解步驟，發(fā)現(xiàn)x+y的值可以無限的增大，求解過程無法終止，判定此最優(yōu)解為無窮大，即x+y是無上界的，因此，更新最優(yōu)解的最小上界為

UA≡y≤3，

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

optT(φ)≡y≤3.

因此，xopt=∞∧yopt≤3.

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

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

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

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

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

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

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

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

5 結(jié)論與展望

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

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

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

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

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

[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)(陳力, 王永吉, 吳敬征, 等. 基于樹狀線性規(guī)劃搜索的單調(diào)速率優(yōu)化設(shè)計[J]. 軟件學(xué)報, 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)(王建新, 管利娜, 江國紅. 可滿足性問題的研究綜述[J]. 計算技術(shù)與自動化, 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ù)簡述[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)(許道云, 劉長云. 帶文字改名策略的 DPLL 算法[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)(林惠民, 張文輝. 模型檢測: 理論, 方法與應(yīng)用[J]. 電子學(xué)報, 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)(趙燕妮, 邊計年, 鄧澍軍. 利用 SMT 約束分解方法求解 RTL 可滿足性問題[J]. 計算機輔助設(shè)計與圖形學(xué)學(xué)報, 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求解器的路徑敏感程序驗證[J]. 軟件學(xué)報, 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)(李舟軍, 張俊賢, 廖湘科, 等. 軟件安全漏洞檢測技術(shù)[J]. 計算機學(xué)報, 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

國家自然科學(xué)基金項目(61170072，61303057)；中國科學(xué)院、國家外國專家局創(chuàng)新團隊國際合作伙伴計劃 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