一種自適應(yīng)的循環(huán)不變式生成方法

劉自恒，曾慶凱,b

(南京大學(xué) a.計算機(jī)科學(xué)與技術(shù)系；b.計算機(jī)軟件新技術(shù)國家重點實驗室，南京 210093)

1 概述

軟件的任何漏洞都可能導(dǎo)致非常嚴(yán)重的后果。無論是軟件設(shè)計人員還是軟件的用戶，均希望在軟件系統(tǒng)投入在正式使用之前，能得到軟件正確性的保證。通過測試可以在一定程度上保證軟件的正確性，但成本較高，不能完全保證軟件的可靠，而且測試只能發(fā)現(xiàn)程序中的錯誤，不能證明程序無錯。從另一個角度考慮，如果可以從理論上證明程序符合預(yù)期的行為或者沒有某種錯誤，同樣可以認(rèn)為軟件是可靠的。20世紀(jì)50年代出現(xiàn)的形式化方法思想，以嚴(yán)格的數(shù)學(xué)和邏輯理論為基礎(chǔ)，適合于軟件和硬件系統(tǒng)的描述、開發(fā)和驗證。

1967年，F(xiàn)loyd提出采用形式化方法證明程序的正確性，經(jīng)過多年的研究，取得了一系列理論和實踐的重大進(jìn)展。在形式化分析驗證程序時，以Floyd-Hoare邏輯為基礎(chǔ)，將程序轉(zhuǎn)換為抽象模型，進(jìn)行邏輯歸納演繹，驗證程序是否滿足程序規(guī)范。使用形式化的思想對程序進(jìn)行分析驗證并不排斥測試，但可以認(rèn)為它是一種更好的測試框架。在分析驗證時開發(fā)者給出要驗證函數(shù)的規(guī)范，但是在低層次結(jié)構(gòu)上(如基本指令、分支、循環(huán)結(jié)構(gòu)等)需要驗證程序自動地推導(dǎo)這些結(jié)構(gòu)的規(guī)范，表達(dá)出它們實現(xiàn)的語義。對于基本的結(jié)構(gòu)，如賦值和分支，Hoare邏輯已經(jīng)給出了直接的轉(zhuǎn)換規(guī)則；但是循環(huán)結(jié)構(gòu)中需要循環(huán)不變式來證明循環(huán)初始時和執(zhí)行過程中均保持的性質(zhì)，而 Hoare邏輯沒有給出直接的生成循環(huán)不變式的規(guī)則，這是因為并不存在通用的不變式生成規(guī)則。因此，形式化程序分析的一個關(guān)鍵性難點在于程序中循環(huán)結(jié)構(gòu)的存在，而且實際的循環(huán)結(jié)構(gòu)中常常又有嵌套循環(huán)和分支結(jié)構(gòu)，操作的數(shù)據(jù)類型除矢量型變量外，還包含數(shù)組等向量型變量，使得循環(huán)不變式的生成工作變得困難。

本文分析、總結(jié)了當(dāng)前常見的循環(huán)不變式生成方法，并提出一種改進(jìn)的循環(huán)不變式生成方法，并通過實驗評價其分析性能。

2 現(xiàn)有方法

通常對于給定的函數(shù)前置條件和后置條件，不變式并不是唯一的，開發(fā)人員往往增量地得到不變式：首先預(yù)測不變式，然后通過觀察程序行為來逐步細(xì)化預(yù)測的不變式[1]，最終得到驗證所需要的不變式信息。計算循環(huán)不變式的方法主要有下面的幾種。

2.1 基于迭代不動點的計算

使用該方法的技術(shù)有數(shù)據(jù)流分析、模型檢測和抽象解釋等。在計算程序的狀態(tài)轉(zhuǎn)換過程中，連續(xù)地計算直到得到數(shù)據(jù)流方程的最小不動點，當(dāng)發(fā)現(xiàn)程序狀態(tài)不再變化時，認(rèn)為發(fā)現(xiàn)不動點。計算的過程是一個不斷迭代直到收斂的過程。但計算過程的收斂性是不可判定的，因此需要一些技術(shù)來保證和加速收斂的過程，如使用放大算子、提高抽象粒度等。

使用放大算子會導(dǎo)致一定程序的精度損失，因此，要盡可能地延遲使用放大算子的時機(jī)，如使用前向放大[2]，同時在合適的位置再使用縮小算子。其他的加速措施也存在同樣的問題，需要在效率和精度之間取一個合理的平衡點。

2.2 基于參數(shù)化模板

該方法主要針對線性數(shù)值計算程序進(jìn)行。計算時通過程序或開發(fā)者指定目標(biāo)不變式的模板形式，其中變量的系數(shù)未知，稱為模板參數(shù)；程序經(jīng)過抽象解釋映射為抽象域上的轉(zhuǎn)換系統(tǒng)；使用不同的技術(shù)求解模板中的系數(shù)，得到不變式。根據(jù)與結(jié)合求解的技術(shù)不同，又可細(xì)分如下：

(1)與約束求解結(jié)合。首先由開發(fā)者或程序默認(rèn)為循環(huán)指定一個帶參數(shù)的不變式模板，其中變量的系數(shù)未知；隨后采用歸納斷言方法，建立不變式之間以及不變式與循環(huán)的前置條件之間的約束，再利用 Farkas定理[3]，消除約束中出現(xiàn)的程序變量，并表達(dá)出循環(huán)相關(guān)的條件，得到關(guān)于模板參數(shù)的非線性約束，從而將線性循環(huán)不變式構(gòu)造問題轉(zhuǎn)化為約束求解問題。最后，使用因式分解、線性規(guī)劃或非線性求解器等方法求參數(shù)的數(shù)值解?；诩s束的方法相對于基于不動點計算的方法有如下優(yōu)點：目標(biāo)指向性明確，效率更高。不需要使用難以控制的放大方法，精確損失小[4]。

(2)與可滿足性(Satisfiability,SAT)求解結(jié)合。先將約束化為合取范式，然后利用Farkas定理消除約束中的程序變量，再將約束中的參數(shù)建模為比特向量(bit-vector)，進(jìn)而將該約束轉(zhuǎn)化為布爾公式，使用SAT求解器搜索滿足約束的參數(shù)值。該方法受益于SAT求解技術(shù)的進(jìn)步。

(3)與量詞消去結(jié)合[5-6]。如果通過循環(huán)完成對數(shù)組的操作，則不變式公式中將含有量詞，無法直接使用約束求解或SAT求解，需要先將其中的量詞消去得到與之等價的不包含量詞的公式，然后再使用約束求解或SAT求解的方法來解。

面向驗證性質(zhì)的增量式歸納不變式構(gòu)造方法[7]。該方法根據(jù)驗證不成立時，求解器返回的虛假反例增量式地生成歸納的不變式，這樣提高了生成不變式的效率，能夠得到剛好滿足驗證需求的不變式性質(zhì)。

在基于參數(shù)化模板的不變式生成方法中，增加模板大小可以有更大機(jī)會使得前置條件適應(yīng)模板，但會生成更大的 SAT式子要求解[4]，使得求解所需的時間和空間變大。對于模板形式的選擇，文獻(xiàn)[4,8-9]由用戶指定不變式模板(同時程序提供了默認(rèn)的模板可以使用)，文獻(xiàn)[4]既可以由用戶指定模板(如指定未知關(guān)系式析取范式表示中合取和析取數(shù)量的最大值)，也提供了一種迭代增加模板大小的方案，直到發(fā)現(xiàn)某個解。適用范圍方面，文獻(xiàn)[10]只處理簡單while程序并針對線性算術(shù)運算，文獻(xiàn)[11-12]只能處理一個簡化了的程序語言，等同于一個C語言的子集，文獻(xiàn)[13]擴(kuò)大了文獻(xiàn)[11]的適應(yīng)范圍。

這種生成不變式方法并不是歸納的，求解之前需要開發(fā)者給出正確的模板形式；應(yīng)用擴(kuò)展性受限于約束求解器的求解能力；對于這種生成方式，用戶指定的模板形式固定，需要與用戶交互，對使用者來講比較繁瑣，適應(yīng)性不強(qiáng)。

2.3 基于機(jī)器學(xué)習(xí)和實際執(zhí)行的方法

文獻(xiàn)[1,14]提出可以通過機(jī)器學(xué)習(xí)的方法來推斷循環(huán)不變式。而Daikon[15]是動態(tài)不變式發(fā)現(xiàn)器，可以探測包括C、C++、Java、Perl語言編寫的程序和含有記錄型結(jié)構(gòu)的數(shù)據(jù)類型。

3 改進(jìn)方法

通過前面的介紹可以發(fā)現(xiàn)，現(xiàn)有的不變式生成方法存在以下不足：(1)處理程序能力往往有限，通常假定處理某個簡單的程序語言，應(yīng)對復(fù)雜的C語言能力不足。(2)使用了參數(shù)化模板求解的方法，其靈活性不足，需要開發(fā)者在對程序深刻理解的基礎(chǔ)上指定模板形式，然后對模板系數(shù)求解，不能自動地考慮程序中的操作語義信息。(3)現(xiàn)有的方法有的只關(guān)注循環(huán)內(nèi)容本身，有的除循環(huán)外只關(guān)注了循環(huán)外的某一點信息，沒有綜合考慮函數(shù)規(guī)范、循環(huán)本身、循環(huán)后操作等內(nèi)容，使得生成的不變式不夠全面。(4)現(xiàn)有的工作沒有從執(zhí)行不變式生成分析，其分析結(jié)果是否使得函數(shù)規(guī)范得以順利完成驗證方面進(jìn)行檢驗，而這正是進(jìn)行不變式生成分析的原始出發(fā)點，現(xiàn)有工作缺乏一定的實踐性評估。

本文提出以下改進(jìn)思路，基于條件賦值轉(zhuǎn)換和自適應(yīng)模板規(guī)則生成循環(huán)不變式，在生成過程中綜合考慮函數(shù)規(guī)范、循環(huán)本身、循環(huán)后操作等信息，這樣能更有針對性地、自動地發(fā)現(xiàn)潛在的循環(huán)不變式，但這種分析是一種保守的分析，會產(chǎn)生并不正確的不變式，需要進(jìn)行驗證；對分析的結(jié)果，除了評價不變式本身的正確性外，還從程序驗證的角度，根據(jù)分析結(jié)果是否使得驗證順利完成，對其有效性進(jìn)行分析。

3.1 條件賦值轉(zhuǎn)換

基于條件賦值轉(zhuǎn)換控制流的思想，這里提出一種條件賦值轉(zhuǎn)換的方法。對于循環(huán)中的每一條賦值語句，直接根據(jù)分支條件和賦值操作類型的不同，轉(zhuǎn)換得到不同的候選不變式，轉(zhuǎn)換的規(guī)則主要有下面的幾種，本文參考文獻(xiàn)[16]的一些做法，執(zhí)行一些變量變換。這里假定循環(huán)開始時變量x的取值范圍為集合x0，它可以是離散的集合，也可能是連續(xù)的區(qū)間；P表示更新操作的內(nèi)容，包含四則運算、指針引用等。標(biāo)量變量指只包含一個值的變量，如C語言中的基本數(shù)據(jù)類型，矢量變量指包含一系列值的變量，如數(shù)組。這里不考慮包含用戶自定義數(shù)據(jù)類型的賦值操作。

(1)分支判斷條件和賦值操作都是標(biāo)量型變量操作(非數(shù)組、指針變量)：

(2)分支判斷條件為標(biāo)量型變量，賦值操作為數(shù)組訪問操作，若數(shù)組A長度為len：

(3)分支判斷條件是關(guān)于下標(biāo)的判斷，賦值操作為數(shù)組訪問操作，若數(shù)組A長度為len：

(4)分支判斷條件是關(guān)于數(shù)組元素值的，賦值操作為數(shù)組訪問操作，若數(shù)組A長度為len：

(5)分支判斷條件是關(guān)于同一數(shù)組元素之間值的，賦值操作為數(shù)組訪問操作，若數(shù)組A長度為len：

(6)分支判斷條件是關(guān)于2個數(shù)組元素之間值的，賦值操作為數(shù)組訪問操作，若數(shù)組A長度為len1，數(shù)組B長度為len2：

在上面的轉(zhuǎn)換規(guī)則中，如果數(shù)組的長度不能確定，則排除對于下標(biāo)表達(dá)式上界的約束表達(dá)。

正確性說明。以第(1)條規(guī)則為例，其他的與之類似。結(jié)果由兩部分構(gòu)成。當(dāng)變量x∈x0時即變量在初始值范圍內(nèi)時，由于未執(zhí)行賦值操作，具有屬性y!=P；當(dāng)變量值不在初始值范圍內(nèi)時，認(rèn)為是在循環(huán)中，當(dāng)滿足路徑條件f(x) ＞0時，執(zhí)行賦值操作，因而有 f(x) ＞0? y=P。這些轉(zhuǎn)換規(guī)則是對于程序語義的直觀的邏輯轉(zhuǎn)換，同時通過變量轉(zhuǎn)換等方式表達(dá)了有關(guān)數(shù)組下標(biāo)變換的屬性；但由于忽略了變量間的別名關(guān)系、變量的值范圍分析并不總是準(zhǔn)確等元素，導(dǎo)致轉(zhuǎn)換結(jié)果存在過近似的問題，因此需要驗證其正確性。

3.2 自適應(yīng)模板生成

這里的模板生成不變式的方法和前面的有所不同，不是根據(jù)指定的模板形式求解未知的模板變量系數(shù)，而是以一種啟發(fā)式的方法生成模板形式表達(dá)的候選不變式。本文希望從程序的語義信息出發(fā)，結(jié)合程序變量的取值情況，使用模板形式表達(dá)出變量之間存在的約束關(guān)系。而模板變量的系數(shù)則從程序中提取得到。這樣可以自動地尋找程序中最有可能存在的不變式約束關(guān)系，適應(yīng)具體程序的語義特點，不需要用戶來指定模板的形式。但這種表達(dá)可能不是精確的，也可能是錯誤的，因而需要驗證其真假，驗證的過程可以由定理證明器完成，也可以在計算不動點時根據(jù)程序的狀態(tài)在抽象域上求解模板約束關(guān)系是否可滿足。

這些啟發(fā)式生成的循環(huán)不變式是根據(jù)從程序中提取到的信息按照生成規(guī)則得到的，這些信息包括要驗證的程序規(guī)范、程序中的屬性斷言、程序變量操作的方式、程序變量可能的系數(shù)、程序變量的取值范圍等。因此，如果可以進(jìn)行更加細(xì)節(jié)的操作分類，提出更多的模板生成規(guī)則，則可以發(fā)現(xiàn)更多的不變式。

目前定義的生成規(guī)則主要從以下方面考慮：

(1)根據(jù)預(yù)定義謂詞生成，判斷某組變量是否可以使得該謂詞屬性成立，判斷由定理證明器判斷，這些謂詞一般是比較簡單的屬性，如判斷某個變量取值是否單調(diào)變化、數(shù)組中的元素是否相等；這里判斷的變量類型必須是和謂詞中的變量類型相兼容的。

(2)被調(diào)用函數(shù)是否有函數(shù)規(guī)范，如果有將相應(yīng)的參數(shù)變量應(yīng)用于規(guī)范中的謂詞中，則得到被調(diào)用函數(shù)的操作結(jié)果。如果沒有函數(shù)規(guī)范，則忽略函數(shù)調(diào)用。被調(diào)用函數(shù)的函數(shù)規(guī)范是其后置條件，表達(dá)了調(diào)用它對變量產(chǎn)生的“影響”，是函數(shù)具體內(nèi)容的一種摘要表示。因此，這里的分析是一種使用了函數(shù)摘要的半過程間的分析。

(3)收集程序中的常量信息，主要是函數(shù)規(guī)范中、循環(huán)后斷言和條件判斷中的常量。

(4)根據(jù)從循環(huán)體內(nèi)、循環(huán)后的 assert語句和其他分支判斷條件收集到的變量和變量的系數(shù)信息，生成變量間可能的模板約束關(guān)系。如果分析關(guān)注的變量集Var，個數(shù)為N；對于長度T的模板，即從Var中選擇T個變量組成模板。但有的抽象域限制系數(shù)值和變量數(shù)量，如八邊形域中限制變量系數(shù)只能為1、0或者?1，限制模板變量數(shù)量為2。

當(dāng)生成模板時，從Var中選擇指定數(shù)量的變量作為模板變量，枚舉選定的模板變量的所有系數(shù)組合，對于系數(shù)不為0的變量，累加其最大值(最小值)的和。生成的模板具有如下形式：

其中，op ∈{＞,≥,==,!=},ci∈ coefv,c∈Const∪{m in,m ax}，cofv是變量v的候選系數(shù)集合，Const是收集到的常數(shù)值集合，min、max分別是選定的系數(shù)不為0的模板變量的最小值、最大值。

3.3 優(yōu)化措施

從分析處理的范圍和方法可知，分析驗證的復(fù)雜度不僅與程序規(guī)模有關(guān)，更與要分析的變量個數(shù)、模板中變量的個數(shù)、每個模板變量候選的系數(shù)個數(shù)有關(guān)。在模板大小一定時，當(dāng)程序規(guī)模較大、要分析的變量增多時，需要驗證的情況急劇增加；而增大模板尺寸時，需要驗證的情況也會急劇增加。如果有N個變量，每個Vair變量有ni個候選的系數(shù)，提取到C個常數(shù)，由之前的模板生成規(guī)則，如果模板里面最多可以含有T個變量(即模板尺寸為T)，則最多需要枚舉驗證種情況，可以看出其具有較高的復(fù)雜度，因此為了使分析過程及時有效地終止，需要執(zhí)行一些剪枝優(yōu)化策略，以壓縮要分析驗證的不變式數(shù)量，本文采用的策略如下：

(1)控制關(guān)注的變量數(shù)量。分析時不分析過程中所有的變量，只分析當(dāng)前循環(huán)中使用的變量、循環(huán)后條件中的變量，除此之外的變量與當(dāng)前循環(huán)的關(guān)聯(lián)性較弱。忽略不能處理的數(shù)據(jù)類型(如結(jié)構(gòu)體)變量。當(dāng)有循環(huán)嵌套時，該策略避免了大量的重復(fù)分析。從其復(fù)雜度公式可以看出，減小分析的變量數(shù)量可以縮減模板數(shù)量。

(2)限制模板尺寸T。當(dāng)T增大時(T＜N /2)，C隨之增大。驗證者可以指定模板的尺寸，例如這里默認(rèn)設(shè)定為3，即模板中最多含有 3個變量。從其復(fù)雜度公式可以看出，減小模板尺寸可以縮減模板數(shù)量。

(3)屏蔽指針本身的分析，只關(guān)注指針指向變量的值即指針引用。忽略非標(biāo)準(zhǔn)數(shù)據(jù)類型，如結(jié)構(gòu)體、枚舉等類型變量。將數(shù)組元素和一般標(biāo)量變量的操作區(qū)分開來，不放在同一個模板中。這樣可以減少候選的不變式模板個數(shù)。

(4)使用改進(jìn)的搜索策略?；镜乃枷胧牵喝绻鸌＞0成立，則I ≥0一定成立，不需要再驗證，而且它是冗余的，只需要返回I＞0即可；如果I＞0成立，則I≤0一定不成立，它們是互斥的。判斷過程如下。

(5)在生成模板時，首先執(zhí)行依賴分析，判斷變量之間是否有依賴關(guān)系(包括數(shù)據(jù)依賴和控制依賴)，不存在依賴關(guān)系時認(rèn)為它們之間聯(lián)系較弱，不應(yīng)該一同構(gòu)成循環(huán)不變式。

4 實現(xiàn)與實驗結(jié)果

4.1 loopInv設(shè)計與實現(xiàn)

本文基于Frama-C平臺和APRON庫對上述方法做了實現(xiàn)，作為一個插件 loopInv集成在 Frama-C中。其在Frama-C的位置和處理流程如圖1所示，其內(nèi)部結(jié)構(gòu)如圖2所示。

圖1 loopInv分析框架

圖2 loopInv框架設(shè)計

預(yù)處理階段完成的工作有：收集要驗證的函數(shù)規(guī)范、數(shù)組變量信息、循環(huán)中的分支條件和其后的斷言條件集合、程序中的常量信息、模板變量的候選系數(shù)集合、循環(huán)中賦值語句的路徑約束條件等信息。在生成轉(zhuǎn)換系統(tǒng)時，循環(huán)中加入模板約束表達(dá)式。驗證時使用 WP插件和 APRON庫可滿足性求解。

4.2 實驗結(jié)果

實驗中選取了2組程序進(jìn)行分析，評估loopInv的有效性。一組是簡單的示例程序，對于這類程序同時用其他不變式生成工具進(jìn)行分析，或分析符合工具特定要求的與之等價的程序，和loopInv對比實驗結(jié)果，這里使用的對比工具是invGen[8]和gin-pink[16]；這些程序來自其他文獻(xiàn)，或出自 WP的測試程序，先將手工書寫的循環(huán)不變式去除；另一部分是規(guī)模較大的實際的開源C程序，由于對比工具或者還不能處理這樣規(guī)模的程序，或者進(jìn)行等價轉(zhuǎn)換工作量較大，不再進(jìn)行對比分析，這里側(cè)重關(guān)注發(fā)現(xiàn)的不變式數(shù)量，不再驗證函數(shù)規(guī)范。

選用的測試對象如表1、表2所示。這里變量個數(shù)是指作為模板變量的變量數(shù)量。

表1 測試程序1

表2 測試程序2

分別設(shè)定模板尺寸為 2和 3，得到的實驗結(jié)果分別如表3和表4所示。其中，列C1～C8分別表示程序編號、輸出不變式個數(shù)、實際正確不變式個數(shù)、錯誤不變式個數(shù)、經(jīng)分析后程序是否得到證明、分析執(zhí)行時間(s)、總的執(zhí)行時間(即包含驗證不變式時間，時:分:秒)、峰值內(nèi)存(MB)。

表3 loopInv實驗結(jié)果統(tǒng)計1

表4 loopInv實驗結(jié)果統(tǒng)計2

同時，選擇工具invGen和gin-pink對程序1～程序6進(jìn)行不變式分析，得到的結(jié)果如表 5所示。其中，列Ca～Ce分別表示程序編號、輸出不變式個數(shù)、程序是否得證、總的執(zhí)行時間(分:秒)、峰值內(nèi)存(MB)；各個統(tǒng)計項的第 1列是 invGen的分析結(jié)果，第 2列是 gin-pink的分析結(jié)果，gin-pink輸出不變式個數(shù)一列中，括號外表示候選的不變式個數(shù)，括號內(nèi)表示正確的不變式個數(shù)。

表5 其他工具分析結(jié)果統(tǒng)計

從實驗結(jié)果可以看出，通過分析，多數(shù)函數(shù)規(guī)范得到了驗證，說明分析過程是有效的；模板尺寸的變大時生成的不變式數(shù)量急劇增多，這能夠發(fā)現(xiàn)更多的循環(huán)不變式，但同時求解所需要的時間和空間都發(fā)生了增長，特別是求解時間增長很快；而實驗結(jié)果也表明，設(shè)定較小的模板尺寸時，得到的不變式分析結(jié)果也可以滿足多數(shù)驗證的需求；求解需要的時間和空間不僅與程序規(guī)模陒關(guān)，更加與程序本身的操作方式陒關(guān)。當(dāng)程序變量數(shù)量較多、操作變化靈活、程序結(jié)構(gòu)變化復(fù)雜、變量中含有數(shù)組等類型時，需要分析的情況增多，分析的難度也隨之上升；陒比invGen和gin-pink，loopInv具有更好的適應(yīng)性和有效性。

5 結(jié)束語

針對當(dāng)前自動生成循環(huán)不變式方法存在的一些局限性，本文綜合考慮函數(shù)規(guī)范、循環(huán)本身、循環(huán)后操作等信息，提出一種基于條件賦值轉(zhuǎn)換和自適應(yīng)模板生成技術(shù)的生成方法，并設(shè)計實現(xiàn)了一個Frama-C的插件loopInv。實驗結(jié)果表明，該方法具有良好的適應(yīng)性，能夠使得實驗中的大部分程序驗證過程順利完成。今后需要在細(xì)化分析程序操作的基礎(chǔ)上，進(jìn)一步完善不變式生成規(guī)則，同時優(yōu)化分析過程，以適應(yīng)更大規(guī)模的程序。

[1]Jung Y,Kong S,Wang B,et al.Deriving Invariants by Algorithmic Learning,Decision Procedures,and Predicate Abstraction[C]//Proc.of the 11th International Conference on Verification,Model Checking,and Abstract Interpretation.Madrid,Spain: Springer,2010.

[2]Gopan D,Reps T W.Lookahead Widening[C]//Proc.of the 18th International Conference on Computer Aided Verification.Seattle,USA: Springer,2006.

[3]Bradley A R,Manna Z,Sipma H B.Linear Ranking with Reachability[C]//Proc.of the 17th International Conference on Computer Aided Verification.Edinburgh,UK: Springer,2005.

[4]Gulwani S,Srivastava S,Venkatesan R.Program Analysis as Constraint Solving[C]//Proc.of ACM SIGPLAN Conference on Programming Language Design and Implementation.Tucson,USA: ACM Press,2008.

[5]Kapur D.Automatically Generating Loop Invariants Using Quantifier Elimination[J].Deduction and Applications,2006,64(1): 54-75.

[6]Monniaux D.A Quantifier Elimination Algorithm for Linear Real Arithmetic[C]//Proc.of the 15th International Conference on Logic for Programming,Artificial Intelligence,and Reasoning.Doha,Qatar: Springer,2008.

[7]Bradley A R,Manna Z.Property-directed Incremental Invariant Generation[J].Formal Aspects of Computing,2008,20(4):379-405.

[8]Gupta A,Rybalchenko A.InvGen: An Efficient Invariant Generator[C]//Proc.of the 21th International Conference on Computer Aided Verification.Grenoble,France: Springer,2009.

[9]Hart T E,Ku K,Gurfinkel A,et al.Ptyasm: Software Model Checking with Proof Templates[C]//Proc.of the 23th IEEE/ACM International Conference on Automated Software Engineering.L'Aquila,Italy: IEEE Press,2008.

[10]Podelski A,Rybalchenko A.A Complete Method for the Synthesis of Linear Ranking Functions[C]//Proc.of the 5th International Conference on Verification,Model Checking,and Abstract Interpretation.Venice,Italy: Springer,2004.

[11]Lalire G,Argoud M,Jeannet B.Interproc[EB/OL].(2008-10-21).http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html.

[12]Moy Y,Marché C.Modular Inference of Subprogram Contracts for Safety Checking[J].Journal of Symbolic Computation,2010,45(11): 1184-1211.

[13]邢建英,李夢君,李舟軍.CILinear: 一個陑性不變式自動構(gòu)造工具[J].計算機(jī)科學(xué),2010,37(12): 91-95.

[14]Jung Y,Kong S,David C,et al.Automatically Inferring Loop Invariants via Algorithmic Learning[C]//Proc.of MSCS’12.[S.1.]: IEEE Press,2012.

[15]Ernst M D,Perkins J H,Guo P J,et al.The Daikon System for Dynamic Detection of Likely Invariants[J].Science of Computer Programming,2007,69(1-3): 35-45.

[16]Furia C A,Meyer B.Inferring Loop Invariants Using Postconditions[M].Berlin,Germany: Springer [s.n.],2010.

[17]Sharma R,Dillig I,Dillig T,et al.Simplifying Loop Invariant Generation Using Splitter Predicates[C]//Proc.of the 23th International Conference on Computer Aided Verification.Cliff Lodge,USA: Springer,2011.

[18]Kovács L,Voronkov A.Finding Loop Invariants for Programs over Arrays Using a Theorem Prover[C]//Proc.of the 12th International Conference on Fundamental Approaches to Software Engineering.York,UK: Springer,2009.