SMT求解技術的發展及最新應用研究綜述

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

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

?

SMT求解技術的發展及最新應用研究綜述

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

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

(wangchong@nfs.iscas.ac.cn)

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

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

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

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

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

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

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

1) 核心算法、數據結構以及現代微處理器的發展使得SAT求解器[33]可以處理含有數萬變量的公式，以SAT求解器為基礎的SMT求解技術隨之提升；

2) SMT求解技術的廣泛應用前景使得各個科研機構積極開發SMT求解器；

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

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

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

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

1 SAT問題及判定算法

1.1 SAT問題

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

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

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

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

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

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

1.2 SAT問題判定算法

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

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

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

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

pure-literal規則用于化簡公式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規則化簡f；

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

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

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

現代DPLL搜索算法均是在此基礎上進行改進的，典型的基于沖突檢測的子句學習求解算法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算法的最大區別在于每當UnitPropagation執行完成后，ConflictDetetction便會檢測是否存在沖突，若存在沖突，則調用ConflicAnalysis分析沖突產生的原因并進行子句學習，以此確定回溯的層次.

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

2 SMT問題及判定算法

2.1 SMT問題及背景理論

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

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

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

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

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

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

在目前的實際應用中，主流SMT求解器支持并實現的主要理論有6個:

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

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

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

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

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

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

x1-x2⊙J，

(1)

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

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

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

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

(2)

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

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

以上介紹了目前應用較為廣泛的主流理論，SMT-LIB目前支持的理論及相互之間的關系如圖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理論之間的關系[55]

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

2.2 組合背景理論求解方法

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

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

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

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

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

2.3 SMT問題判定算法

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

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

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

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

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

2.3.2 求解SMT問題的惰性算法

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

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

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

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

此算法的優勢在于，若算法在步驟2中已判定SAT公式不可滿足，則無需進行后續判定工作，提高了求解效率.惰性算法是SAT求解器與對應的背景理論相結合的產物，典型的惰性算法是DPLL(T)[70-71]算法.

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

算法2. DPLL(T).

輸入：SMT公式F；

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

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

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

3 SMT求解器及性能比較

隨著SMT背景理論的逐漸成熟以及SMT問題判定算法的不斷發展，許多SMT求解器能夠滿足學術界的研究需求，一些成熟的SMT求解器也能處理大規模工業化的應用問題.目前主要的求解器有：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以其優秀的綜合求解能力被業界所認可，是目前為止在擴展性、表達能力以及求解效率等方面都較為出色的SMT求解器.Z3的求解框架集成了基于DPLL的SAT求解器，并支持未解釋函數、算術運算、數組等背景理論，核心求解算法是DPLL(T)算法和DTC方法.許多工業界的項目都用到了Z3，例如Pex[39]，HAVOC[81]，Yogi[82]，SLAMSDV[83]，Vigilante[84]等.

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

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

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

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

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

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

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

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

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

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

4 SMT應用

隨著SMT判定算法的不斷發展以及SMT求解器的逐漸成熟，人們開始使用SMT解決一些實際問題，例如測試用例自動生成、程序缺陷檢測、RTL驗證、程序分析與驗證、線性邏輯約束公式優化問題求解等.

4.1 測試用例自動生成

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

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

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

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

4.1.2 具體示例

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

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

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

(9)

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

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

(10)

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

Fig. 3 Record the number of requests
圖3 記錄請求次數

4.1.3 SMT在測試用例自動生成中的應用

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

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

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

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

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

4.2 程序缺陷檢測

4.2.1 基于SMT的程序缺陷檢測

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

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

4.2.2 具體示例

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

Fig. 4 Converting the source code into the SMT formula
圖4 源程序轉化為SMT公式

4.2.3 SMT在程序缺陷檢測中的應用

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

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

Fig. 5 Overview of the ESBMC architecture圖5 ESBMC結構概覽

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

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

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

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

4.3 RTL驗證

4.3.1 基于SMT的RTL驗證

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

4.3.2 具體示例

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

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

4.3.3 SMT在RTL驗證中的應用

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

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

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

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

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

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

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

Kunapareddy等人[10]對LPSAT和SMT在RTL驗證中的應用進行了比較，結論表明：基于Z3的RTL驗證方法在代碼復雜度、執行時間和迭代次數上的表現均優于LPSAT方法.

4.4 程序分析與驗證

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

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

4.4.2 具體示例

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

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

4.4.3 SMT在程序分析與驗證中的應用

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

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

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

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

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

4.5 線性邏輯約束公式優化問題求解

4.5.1 SMT與線性邏輯約束公式優化問題求解

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

4.5.2 具體示例

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

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

(11)

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

1) 假設最優解為optT(φ)，根據約束條件φ可將最優解的最小上界(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]=?，因為此點不接觸任一邊界.提取目標函數H的第1個元素y，判斷在滿足y≤3的基礎上，是否存在優于可行解p1的另1個可行解p2，即:

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

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

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

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

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

5) 提取目標函數H的第2個元素x+y，在滿足x+y≤∞的基礎上，使用SMT求解器求得優于p3的可行解p4=(6,3)，重復此求解步驟，發現x+y的值可以無限的增大，求解過程無法終止，判定此最優解為無窮大，即x+y是無上界的，因此，更新最優解的最小上界為

UA≡y≤3，

此時，UA≡OA，求解結束，得到最優解為

optT(φ)≡y≤3.

因此，xopt=∞∧yopt≤3.

4.5.3 SMT在線性約束優化問題求解中的應用

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

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

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

4.6 基于SMT的其他應用

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

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

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

5 結論與展望

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

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

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

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

對于SMT求解器本身而言，大多數SMT求解器只接受無量詞一階邏輯公式作為輸入，實際問題中經常會含有全稱量詞(?)，求解此類問題是目前SMT求解器的難點之一，僅有少數幾個主流的SMT求解器支持帶有全稱量詞問題的求解，比如Z3，CVC4等.求解方法主要分為2種：1)基于模式(pattern-based)的量詞實例化方法，主要是將帶有全稱量詞的變量實例化為帶有存在量詞(?)的變量，比如將(?x,x>1)實例化為(?x=2,x>1).但是如何選取x的具體實例化數值是有待研究的問題.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)(陳力, 王永吉, 吳敬征, 等. 基于樹狀線性規劃搜索的單調速率優化設計[J]. 軟件學報, 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]. 計算技術與自動化, 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求解技術簡述[J]. 計算機科學與探索, 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]. 計算機科學與探索, 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)(林惠民, 張文輝. 模型檢測: 理論, 方法與應用[J]. 電子學報, 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]. 計算機輔助設計與圖形學學報, 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]. 軟件學報, 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)(李舟軍, 張俊賢, 廖湘科, 等. 軟件安全漏洞檢測技術[J]. 計算機學報, 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

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