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

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

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

【參考文獻】

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

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

【共引文獻】

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

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

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

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

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

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

【二級參考文獻】

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

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

【相似文獻】

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

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

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

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

4 張學舟;;反向驗證帶切變的線性時段不變式[J];科技視界;2013年34期

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

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

7 楊瀟瀟;段振華;;良基歸納法在時序邏輯程序不變式驗證中的應用[J];計算機科學;2009年06期

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：1182230