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

【摘要】：可滿足性模理論(satisfiability modulo theories,SMT)是判定一階邏輯公式在組合背景理論下的可滿足性問(wèn)題.SMT的背景理論使其能很好地描述實(shí)際領(lǐng)域中的各種問(wèn)題,結(jié)合高效的可滿足性判定算法,SMT在測(cè)試用例自動(dòng)生成、程序缺陷檢測(cè)、RTL(register transfer level)驗(yàn)證、程序分析與驗(yàn)證、線性邏輯約束公式優(yōu)化問(wèn)題求解等一些最新研究領(lǐng)域中有著突出的優(yōu)勢(shì).首先闡述SMT問(wèn)題的基礎(chǔ)SAT(satisfiability)問(wèn)題及判定算法;其次對(duì)SMT問(wèn)題、判定算法進(jìn)行了總結(jié),分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后著重介紹了SMT求解技術(shù)在典型領(lǐng)域中的實(shí)際應(yīng)用,對(duì)目前的研究熱點(diǎn)進(jìn)行了闡述;最后對(duì)SMT未來(lái)的發(fā)展前景進(jìn)行了展望,目的是試圖推動(dòng)SMT的發(fā)展,為此領(lǐng)域的相關(guān)人員提供有益的參考.
[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ǔ)軟件國(guó)家工程研究中心(中國(guó)科學(xué)院軟件研究所);中國(guó)科學(xué)院大學(xué);計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室(中國(guó)科學(xué)院軟件研究所);中央財(cái)經(jīng)大學(xué)信息學(xué)院;
【基金】：國(guó)家自然科學(xué)基金項(xiàng)目(61170072,61303057) 中國(guó)科學(xué)院、國(guó)家外國(guó)專家局創(chuàng)新團(tuán)隊(duì)國(guó)際合作伙伴計(jì)劃~~
【分類號(hào)】：TP301.6;TP311.53

【參考文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

【共引文獻(xiàn)】

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

1 王，

本文編號(hào)：1702879