發(fā)布時間：2018-04-03 00:38

  本文選題：可滿足性模理論　切入點：SMT求解器　出處：《計算機研究與發(fā)展》2017年07期

【摘要】：可滿足性模理論(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)人員提供有益的參考.
[Abstract]:Satisfiability modulo the SMTs is the background theory of determining the satisfiability problem of the first-order logic formula under combinatorial background theory, which enables it to describe all kinds of problems in practical fields.Combined with an efficient satisfiability determination algorithm, SMT has outstanding advantages in some new research fields, such as automatic generation of test cases, program defect detection and RTL register transfer level verification, program analysis and verification, optimization of linear logic constraint formula, and so on.At first, the basic problem of SMT problem and its judging algorithm are introduced. Secondly, the SMT problem is summarized, and the mainstream SMT solver, including Z3Yices2CVC4, is analyzed, and the practical application of SMT solution technology in typical field is emphasized.At last, the prospect of the future development of SMT is prospected, with the purpose of trying to promote the development of SMT, and to provide useful reference for the relevant personnel in this field.
【作者單位】： 基礎(chǔ)軟件國家工程研究中心(中國科學(xué)院軟件研究所);中國科學(xué)院大學(xué);計算機科學(xué)國家重點實驗室(中國科學(xué)院軟件研究所);中央財經(jīng)大學(xué)信息學(xué)院;
【基金】：國家自然科學(xué)基金項目(61170072,61303057) 中國科學(xué)院、國家外國專家局創(chuàng)新團隊國際合作伙伴計劃~~
【分類號】：TP301.6;TP311.53

【參考文獻】

相關(guān)期刊論文 前9條

1 陳力;王永吉;吳敬征;呂蔭潤;;基于樹狀線性規(guī)劃搜索的單調(diào)速率優(yōu)化設(shè)計[J];軟件學(xué)報;2015年12期

2 金繼偉;馬菲菲;張健;;SMT求解技術(shù)簡述[J];計算機科學(xué)與探索;2015年07期

3 李舟軍;張俊賢;廖湘科;馬金鑫;;軟件安全漏洞檢測技術(shù)[J];計算機學(xué)報;2015年04期

4 何炎祥;吳偉;陳勇;徐超;;基于SMT求解器的路徑敏感程序驗證[J];軟件學(xué)報;2012年10期

5 趙燕妮;邊計年;鄧澍軍;;利用SMT約束分解方法求解RTL可滿足性問題[J];計算機輔助設(shè)計與圖形學(xué)學(xué)報;2010年02期

6 王建新;管利娜;江國紅;;可滿足性問題的研究綜述[J];計算技術(shù)與自動化;2009年04期

7 許道云;劉長云;;帶文字改名策略的DPLL算法[J];計算機科學(xué)與探索;2007年01期

8 黃拙,張健;由一階邏輯公式得到命題邏輯可滿足性問題實例(英文)[J];軟件學(xué)報;2005年03期

9 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報;2002年S1期

【共引文獻】

相關(guān)期刊論文 前10條

1 王，

本文編號：1702879