本文關(guān)鍵詞：含有析取語義循環(huán)的不變式生成改進(jìn)方法

  更多相關(guān)文章： 抽象解釋 抽象域 不變式 析取語義 循環(huán)分解

【摘要】：抽象解釋為程序不變式的自動(dòng)化生成提供了通用的框架,但是該框架下的大多數(shù)已有數(shù)值抽象域只能表達(dá)幾何上是凸的約束集.因此,對于包含(所對應(yīng)的約束集是非凸的)析取語義的特殊程序結(jié)構(gòu),采用傳統(tǒng)數(shù)值抽象域會(huì)導(dǎo)致分析結(jié)果不精確.針對顯式和隱式含有析取語義的循環(huán)結(jié)構(gòu),提出了基于循環(huán)分解和歸納推理的不變式生成改進(jìn)方法,緩解了抽象解釋分析中出現(xiàn)的語義損失問題.實(shí)驗(yàn)結(jié)果表明:相比已有方法,該方法能為這種包含析取語義的循環(huán)結(jié)構(gòu)生成更加精確的不變式,并且有益于一些安全性質(zhì)的推理.
【作者單位】： 計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室(南京大學(xué));南京大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系;并行與分布處理國防科技重點(diǎn)實(shí)驗(yàn)室(國防科學(xué)技術(shù)大學(xué)計(jì)算機(jī)學(xué)院);
【基金】：國家自然科學(xué)基金(61170070,61572248,61431008,61321491) 國家科技支撐計(jì)劃(2012BAK26B01) 國家高技術(shù)研究發(fā)展計(jì)劃(863)(2011AA1A202)~~
【分類號(hào)】：TP311.1
【正文快照】：

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前1條

1 陳立前;王戟;侯蘇寧;;單變量區(qū)間線性不等式抽象域[J];計(jì)算機(jī)學(xué)報(bào);2010年03期

【共引文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前5條

1 潘建東;陳立前;黃達(dá)明;孫浩;曾慶凱;;含有析取語義循環(huán)的不變式生成改進(jìn)方法[J];軟件學(xué)報(bào);2016年07期

2 魏歐;石玉峰;徐丙鳳;黃志球;陳哲;;軟件模型檢測中的抽象模型研究綜述[J];計(jì)算機(jī)研究與發(fā)展;2015年07期

3 王雅文;宮云戰(zhàn);肖慶;;基于區(qū)間必然集的測試用例生成方法[J];計(jì)算機(jī)輔助設(shè)計(jì)與圖形學(xué)學(xué)報(bào);2013年04期

4 姜加紅;陳立前;王戟;;基于浮點(diǎn)區(qū)間冪集抽象域的浮點(diǎn)程序分析[J];計(jì)算機(jī)科學(xué)與探索;2013年03期

5 崔寶江;梁曉兵;王禹;王建新;;基于回溯與引導(dǎo)的關(guān)鍵代碼區(qū)域覆蓋的二進(jìn)制程序測試技術(shù)研究[J];電子與信息學(xué)報(bào);2012年01期

【二級(jí)參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前1條

1 姬孟洛;王懷民;李夢君;董威;齊治昌;;一種基于抽象解釋和通用單調(diào)數(shù)據(jù)流框架的值范圍分析方法[J];計(jì)算機(jī)研究與發(fā)展;2006年11期

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 王稚慧,屈延文;不變式產(chǎn)生器——程序驗(yàn)證的重要工具[J];計(jì)算機(jī)學(xué)報(bào);1984年03期

2 邢建英;李夢君;李舟軍;;基于不變式生成的循環(huán)停機(jī)性驗(yàn)證[J];計(jì)算機(jī)工程與科學(xué);2012年04期

3 陳妼敏;;Abel型常微分方程的Maple求解[J];黃岡師范學(xué)院學(xué)報(bào);2006年03期

4 張學(xué)舟;;反向驗(yàn)證帶切變的線性時(shí)段不變式[J];科技視界;2013年34期

5 李志武,王安榮;局部公平網(wǎng)的充要條件研究[J];西安電子科技大學(xué)學(xué)報(bào);2002年06期

6 劉清;一種尋找測試值斷言證明程序正確的方法[J];計(jì)算機(jī)工程;1981年03期

7 楊瀟瀟;段振華;;良基歸納法在時(shí)序邏輯程序不變式驗(yàn)證中的應(yīng)用[J];計(jì)算機(jī)科學(xué);2009年06期

8 鄭宇軍;石海鶴;薛錦云;陳勝勇;;基于形式演算和不變式驗(yàn)證的可信算法程序構(gòu)造(英文)[J];中國通信;2011年04期

9 明繼軍,朱關(guān)銘,繆淮扣;Z規(guī)格說明的系統(tǒng)不變式及其抽取[J];上海大學(xué)學(xué)報(bào)(自然科學(xué)版);1999年S1期

10 鄒姝稚;對Wirth一個(gè)不變式的修正[J];河海大學(xué)學(xué)報(bào)(自然科學(xué)版);2000年06期

中國重要會(huì)議論文全文數(shù)據(jù)庫 前1條

1 廖理幾;郝偉;金澤宸;蔣毅堅(jiān);易明;;用張量不變式和協(xié)變式方法計(jì)算非磁性晶體喇曼效應(yīng)的張量元[A];中國物理學(xué)會(huì)光散射專業(yè)委員會(huì)成立十周年暨第六屆學(xué)術(shù)會(huì)議論文集（上）[C];1991年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前1條

1 付春雷;基于OWL2DL本體的OCL不變式語義不一致性自動(dòng)檢測研究[D];重慶大學(xué);2014年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前5條

1 田豐;基于不變式的程序驗(yàn)證工具的設(shè)計(jì)與實(shí)現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2011年

2 王燕妮;基于不變式的軟件故障檢測與恢復(fù)技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2010年

3 楊東曉;基于Daikon的Java程序動(dòng)態(tài)分析技術(shù)研究[D];吉林大學(xué);2004年

4 張愷;模情況下二面體群D_(2p)的不變式環(huán)(?)[V]~(D_(2p))的Transfer理想[D];大連理工大學(xué);2014年

5 羅清勝;OCL約束驗(yàn)證與實(shí)現(xiàn)方法研究[D];江西財(cái)經(jīng)大學(xué);2006年

，

本文編號(hào)：1182230