首頁(yè) > 期刊 > 自然科學(xué)與工程技術(shù) > 信息科技 > 電子信息科學(xué)綜合 > 計(jì)算機(jī)工程與科學(xué) > 基于一階邏輯的可滿(mǎn)足求解方法研究進(jìn)展 【正文】
基于一階邏輯的可滿(mǎn)足求解方法研究進(jìn)展
張建民; 黎鐵軍; 馬柯帆; 肖立權(quán) 國(guó)防科技大學(xué)計(jì)算機(jī)學(xué)院; 湖南長(zhǎng)沙410073
- 形式化驗(yàn)證
- 一階邏輯
- 布爾可滿(mǎn)足
- 可滿(mǎn)足性模理論
摘要：基于命題邏輯的布爾可滿(mǎn)足SAT存在描述能力弱、抽象層次低、求解復(fù)雜度高等問(wèn)題,而基于一階邏輯的可滿(mǎn)足性模理論SMT采用高層建模語(yǔ)言,表達(dá)能力更強(qiáng),更接近于字級(jí)設(shè)計(jì),避免將問(wèn)題轉(zhuǎn)化到位級(jí)求解,在硬件RTL級(jí)驗(yàn)證、程序驗(yàn)證與實(shí)時(shí)系統(tǒng)驗(yàn)證等領(lǐng)域得到了廣泛應(yīng)用。針對(duì)近年來(lái)涌現(xiàn)的眾多SMT求解方法,依據(jù)方法的求解方式進(jìn)行了分類(lèi)與對(duì)比。而后,對(duì)3種主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的實(shí)現(xiàn)進(jìn)行了概要介紹。最后,討論了SMT求解方法當(dāng)前所面臨的主要挑戰(zhàn)以及在SMT求解方面的一些研究成果,并對(duì)今后的研究進(jìn)行了展望。
- 形式化驗(yàn)證
- 一階邏輯
- 布爾可滿(mǎn)足
- 可滿(mǎn)足性模理論
摘要：基于命題邏輯的布爾可滿(mǎn)足SAT存在描述能力弱、抽象層次低、求解復(fù)雜度高等問(wèn)題,而基于一階邏輯的可滿(mǎn)足性模理論SMT采用高層建模語(yǔ)言,表達(dá)能力更強(qiáng),更接近于字級(jí)設(shè)計(jì),避免將問(wèn)題轉(zhuǎn)化到位級(jí)求解,在硬件RTL級(jí)驗(yàn)證、程序驗(yàn)證與實(shí)時(shí)系統(tǒng)驗(yàn)證等領(lǐng)域得到了廣泛應(yīng)用。針對(duì)近年來(lái)涌現(xiàn)的眾多SMT求解方法,依據(jù)方法的求解方式進(jìn)行了分類(lèi)與對(duì)比。而后,對(duì)3種主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的實(shí)現(xiàn)進(jìn)行了概要介紹。最后,討論了SMT求解方法當(dāng)前所面臨的主要挑戰(zhàn)以及在SMT求解方面的一些研究成果,并對(duì)今后的研究進(jìn)行了展望。
注：因版權(quán)方要求，不能公開(kāi)全文，如需全文，請(qǐng)咨詢(xún)雜志社
計(jì)算機(jī)工程與科學(xué)
- 預(yù)計(jì)1-3個(gè)月 預(yù)計(jì)審稿周期
- 0.79 影響因子
- 計(jì)算機(jī) 快捷分類(lèi)
- 月刊 出版周期
主管單位：國(guó)防科技大學(xué);主辦單位：國(guó)防科技大學(xué)計(jì)算機(jī)學(xué)院
我們提供的服務(wù)
在線客服
一對(duì)一咨詢(xún)服務(wù)、簡(jiǎn)單快捷、省時(shí)省力
了解更多 >
快遞配送
直郵到家、實(shí)時(shí)跟蹤、更安全更省心
了解更多 >
雜志訂閱
去除中間環(huán)節(jié)享受低價(jià)，物流進(jìn)度實(shí)時(shí)通知
了解更多 >
雜志推薦
正版雜志，匹配度高、性?xún)r(jià)比高、成功率高
了解更多 >