吳世堂，李 寧，詹海潭

（中國(guó)航天科技集團(tuán)公司第七一○研究所，北京100037）

0 引 言

程序中變量的值范圍信息有助于判斷程序中是否存在除零錯(cuò)誤、數(shù)組越界、整數(shù)溢出等多種運(yùn)行時(shí)錯(cuò)誤。精確獲取變量值范圍是不可能的，必須在精度和效率之間進(jìn)行折中?；诔橄蠼忉尷碚摚?］的數(shù)值程序分析技術(shù)可以給出每個(gè)程序點(diǎn)的數(shù)值變量近似且可靠的值范圍信息。其中基于該理論的抽象域的設(shè)計(jì)是權(quán)衡分析精度和效率的關(guān)鍵。

在航天控制軟件中，往往需要進(jìn)行大量矩陣運(yùn)算，因此對(duì)矩陣的抽象直接影響該類軟件的分析。在已有的抽象域中，有許多對(duì)數(shù)組的抽象，為了降低分析的復(fù)雜性，提高分析效率，一般是將整個(gè)數(shù)組簡(jiǎn)單抽象為單個(gè)數(shù)值變量，即不考慮數(shù)組元素之間的差異性；或者將數(shù)組元素抽象為固定數(shù)目的幾個(gè)數(shù)值變量［2］，每個(gè)部分用一個(gè)數(shù)值概要變量來(lái)抽象，有限考慮了元素之間的差異性，但是仍然極大損失數(shù)組元素精度；還有的提出數(shù)組區(qū)間集的方式來(lái)抽象數(shù)組元素［3］，通過(guò)在整型區(qū)間集的基礎(chǔ)上構(gòu)造數(shù)組區(qū)間集記錄數(shù)組變量值范圍和數(shù)組長(zhǎng)度信息，增加了空間開(kāi)銷；侯蘇寧等提出將數(shù)組中的每個(gè)元素均抽象為一個(gè)數(shù)值變量［4］，雖然提高數(shù)組元素分析的精度，但是分析效率極低，并不適合實(shí)際航天控制軟件的分析［5］。

本文在充分考慮對(duì)航天控制軟件分析中矩陣運(yùn)算的精度重要性，以及分析效率，提出了區(qū)間向量抽象域。通過(guò)將矩陣的各行各列分別抽象為一個(gè)區(qū)間，形成一個(gè)區(qū)間向量對(duì)，用區(qū)間向量對(duì)的對(duì)應(yīng)元素交集表示矩陣元素。同時(shí)，設(shè)計(jì)了一系列域上的操作算子保證分析的精度和效率。本文方法與將矩陣抽象為單個(gè)變量方法和抽象為簡(jiǎn)單幾個(gè)變量方法相比，精度有了很大的提高；與完全展開(kāi)矩陣每個(gè)元素的方法相比，大大減少時(shí)間和空間開(kāi)銷，增加了方法的實(shí)用性。

1 區(qū)間向量抽象域

1.1 區(qū)間向量抽象域的表示

區(qū)間向量抽象域是在經(jīng)典的區(qū)間抽象域基礎(chǔ)上，針對(duì)程序中的數(shù)組變量的表示而進(jìn)行的擴(kuò)展。下面先回顧區(qū)間抽象域的定義。

區(qū)間抽象域是指用值區(qū)間來(lái)描繪程序變量值范圍的抽象狀態(tài)。其符號(hào)通?？梢员硎緸镮nternal＝ ｛⊥｝∪｛［m1，m2］｜m1≤m2，m1∈M∪ ｛－∞｝，m2∈M∪ ｛＋∞｝｝。對(duì)任意m∈M，都可以將m 的大小擴(kuò)展到 （－∞，＋∞）上，即－∞≤m≤＋∞。

基于區(qū)間抽象域［6］的靜態(tài)分析是在所有程序點(diǎn)為每個(gè)變量維護(hù)一個(gè)區(qū)間，用來(lái)刻畫(huà)變量在該程序點(diǎn)的值范圍信息。

為了更準(zhǔn)確的描述變量的值范圍，很多研究提出區(qū)間集的概念［7］。但是仍然沒(méi)有區(qū)別數(shù)組元素之間的差異性，僅僅將數(shù)組變量作為單獨(dú)變量來(lái)處理相對(duì)應(yīng)的區(qū)間集，對(duì)于分析數(shù)組元素運(yùn)算所帶來(lái)的精度損失仍然很大。

矩陣元素是實(shí)數(shù)集的有序集合，而區(qū)間向量［8］是區(qū)間集的有序集合，能夠合理的表示矩陣元素的有序性，在程序靜態(tài)分析中就能夠體現(xiàn)元素之間的差異性，在提高分析的精度的同時(shí)，分析的效率也不會(huì)過(guò)于復(fù)雜，滿足實(shí)際軟件分析的需要。

對(duì)于給定的矩陣 （數(shù)值型二維數(shù)組）A 中假設(shè)包含m×n個(gè)元素，那么首先可以將實(shí)數(shù)矩陣轉(zhuǎn)化為區(qū)間矩陣，然后將矩陣中每一行的n 個(gè)區(qū)間元素由該n 個(gè)元素可能取到的最小值和最大值所構(gòu)成的區(qū)間來(lái)近似表示。將矩陣中每一列的m 個(gè)區(qū)間元素由該m 個(gè)元素可能取到的最小值和最大值所構(gòu)成的區(qū)間來(lái)近似表示。因此，一個(gè)矩陣可以由一個(gè)列區(qū)間向量＝［A1A2… Am］T和一個(gè)行區(qū)間向量＝［Ar1Ar2… Arn］所組成的區(qū)間向量對(duì)＜，＞來(lái)近似表示，其中向量中的元素Ai（i＝1，2，…，m）是矩陣A 的第i 行元素抽象后的形式化表示，Ajr（j ＝1，2，…，n）是矩陣A 第j 列元素抽象后的形式化表示。

由于區(qū)間抽象域［5］在實(shí)數(shù)R 上的區(qū)間集合構(gòu)成了一個(gè)完全格，顯然，區(qū)間向量的集合也構(gòu)成了一個(gè)完全格［Itvects，iv，∩iv，∪iv，⊥iv，┬iv］。基于抽象解釋理論，實(shí)數(shù)矩陣與區(qū)間向量對(duì)抽象域之間的關(guān)系可以通過(guò)下面Galois連接來(lái)表示

式中： （R）——實(shí)數(shù)集合，I——區(qū)間集合， ——矩陣。具體函數(shù)γiv是將區(qū)間向量抽象域向矩陣具體域進(jìn)行具體化的過(guò)程，形式化表示為γiv＝［〈ItvectsT，Itvects〉→ （I（（R）））］，具體化過(guò)程是通過(guò)將行、列兩個(gè)區(qū)間向量對(duì)應(yīng)的區(qū)間元素求交集獲得矩陣中的相對(duì)應(yīng)的矩陣元素，形式化定義如下所示

抽象函數(shù)αiv是將矩陣具體域向區(qū)間向量抽象域進(jìn)行抽象化 的 過(guò) 程。形 式 化 定 義 為αiv＝ ［ （I（ （R）））→〈ItvectsT，Itvects〉］，抽象化的過(guò)程是通過(guò)首先將實(shí)數(shù)矩陣轉(zhuǎn)化為區(qū)間矩陣，形式化表示為： （ （R））→ （I（（R）））。然后將區(qū)間矩陣的每一行的所有區(qū)間元素的可能取值的最小值和最大值作為一個(gè)區(qū)間，表示該行所有元素的可能取值的上界；每一列的所有區(qū)間元素的可能取值的最小值和最大值作為一個(gè)區(qū)間，表示該列所有元素的可能取值的上界。這樣就形成一個(gè)區(qū)間向量對(duì)來(lái)實(shí)現(xiàn)矩陣的抽象過(guò)程。形式化定義如下所示

1.2 區(qū)間向量抽象域的域操作

在基于抽象解釋理論框架下，抽象域是主要內(nèi)容，而支撐抽象域的各種基本操作算子是抽象解釋框架中的抽象域應(yīng)用于實(shí)際程序分析的關(guān)鍵。下面給出在上面定義的區(qū)間向量抽象域上基本操作算子的設(shè)計(jì)。

設(shè)任意給定兩個(gè)實(shí)數(shù)矩陣Am×n 和Bn×t，通過(guò)上面設(shè)計(jì)的抽象化函數(shù)αiv，可以獲得抽象區(qū)間向量對(duì)分別為

區(qū)間向量抽象域是對(duì)實(shí)數(shù)矩陣轉(zhuǎn)化為區(qū)間矩陣后進(jìn)行的抽象，也就是對(duì)區(qū)間抽象域進(jìn)行的擴(kuò)展，因此，在區(qū)間向量抽象域上的操作算子也與區(qū)間抽象域操作算子密切相關(guān)。下面分別詳細(xì)給出該抽象域上的基本操作算子的設(shè)計(jì)。

（1）交操作 （Meet）

兩個(gè)區(qū)間向量之間的交運(yùn)算是指兩個(gè)矩陣的相對(duì)應(yīng)的兩個(gè)元素區(qū)間值范圍進(jìn)行交運(yùn)算。具體過(guò)程為，首先根據(jù)區(qū)間向量對(duì)進(jìn)行具體化操作，分別獲得兩個(gè)區(qū)間矩陣，然后對(duì)獲得的兩個(gè)區(qū)間矩陣相對(duì)應(yīng)的元素求交運(yùn)算。那么矩陣Am×n和Bn×t單個(gè)元素Aij和Bhk交運(yùn)算的形式化定義如下所示

式中：∩i運(yùn)算是區(qū)間抽象域交操作，即兩個(gè)區(qū)間進(jìn)行交操作。

（2）接合操作 （Join）

兩個(gè)區(qū)間向量進(jìn)行接合是指兩個(gè)矩陣的相對(duì)應(yīng)兩個(gè)元素區(qū)間值范圍作并運(yùn)算，具體過(guò)程為，首先根據(jù)區(qū)間向量進(jìn)行具體化操作，分別獲得兩個(gè)區(qū)間矩陣，然后對(duì)獲得的兩個(gè)區(qū)間矩陣相對(duì)應(yīng)的元素求接合。那么矩陣Am×n 和Bn×t單個(gè)元素Aij和Bhk接合運(yùn)算的形式化定義如下所示

式中：∪i運(yùn)算是區(qū)間抽象域接合操作，即兩個(gè)區(qū)間進(jìn)行接合操作。

（3）算術(shù)運(yùn)算操作 （Arithmetic）

兩個(gè)區(qū)間向量的算術(shù)運(yùn)算操作是指兩個(gè)矩陣的相對(duì)應(yīng)的兩個(gè)元素區(qū)間值范圍作算術(shù)運(yùn)算。具體過(guò)程為，首先根據(jù)區(qū)間向量對(duì)進(jìn)行具體化操作，分別獲得兩個(gè)區(qū)間矩陣，然后對(duì)這兩個(gè)區(qū)間矩陣相對(duì)應(yīng)的元素進(jìn)行相應(yīng)的算術(shù)運(yùn)算。那么矩陣Am×n和Bn×t單個(gè)元素Aij和Bhk算術(shù)運(yùn)算的形式化定義的四則運(yùn)算如式 （6）所示

其中，運(yùn)算符⊙i∈｛＋i，－i，×i，÷i｝，均為區(qū)間抽象域上進(jìn)行加、減、乘、除四則運(yùn)算。

如式 （7）為對(duì)矩陣Am×n 單個(gè)元素Aij取反運(yùn)算的形式化表示

其中，運(yùn)算符－i為區(qū)間抽象域上的取反操作。

（4）比較操作 （Compare）

比較是指格上的兩個(gè)數(shù)之間偏序關(guān)系的比較。兩個(gè)區(qū)間向量之間的比較操作是指兩個(gè)矩陣相對(duì)應(yīng)的元素區(qū)間值范圍的比較。具體比較過(guò)程為，首先根據(jù)區(qū)間向量抽象域進(jìn)行具體化操作，分別獲得相應(yīng)區(qū)間矩陣，然后對(duì)區(qū)間矩陣對(duì)應(yīng)的元素進(jìn)行區(qū)間抽象域上的比較操作，形式化表示如下

其中，i是區(qū)間抽象域上的比較操作。（5）拓寬操作 （Widening）

在基于抽象解釋理論進(jìn)行程序靜態(tài)分析過(guò)程中，為了加速程序分析的收斂速度，需要對(duì)抽象域進(jìn)行拓寬操作。而對(duì)表示矩陣的變量進(jìn)行拓寬操作可以表示為對(duì)區(qū)間向量對(duì)的拓寬操作也就是分別對(duì)行區(qū)間向量和列區(qū)間向量進(jìn)行拓寬操作。區(qū)間向量的拓寬操作則是將兩個(gè)區(qū)間向量對(duì)應(yīng)元素之間分別進(jìn)行區(qū)間拓寬操作，區(qū)間向量對(duì)拓寬操作的形式化表示如下

其中，運(yùn)算 i 是區(qū)間抽象域上的標(biāo)準(zhǔn)拓寬操作。（6）遷移函數(shù) （transfer function）

在基于抽象解釋的程序靜態(tài)分析過(guò)程中，遷移函數(shù)是指，程序在執(zhí)行完一條語(yǔ)句之后，程序狀態(tài)發(fā)生的變化在抽象域上所表示的狀態(tài)遷移動(dòng)作。

基于抽象解釋的程序靜態(tài)分析，會(huì)在每個(gè)程序點(diǎn)創(chuàng)建一個(gè)抽象環(huán)境，用X＃表示，即把所有程序變量映射到抽象域。對(duì)于C語(yǔ)言中的基本類型的變量都可以映射到區(qū)間抽象域，但是對(duì)于表示矩陣的變量，在實(shí)際程序中并不存在直接矩陣類型，而往往是使用數(shù)組表示。矩陣運(yùn)算操作的完成也是通過(guò)若干次的數(shù)組元素運(yùn)算來(lái)完成。下面討論使用二維數(shù)組表示矩陣，且程序中采用數(shù)組下標(biāo)訪問(wèn)方式對(duì)數(shù)組元素進(jìn)行操作情況下的區(qū)間向量抽象域上的遷移函數(shù)的操作。

在程序分析過(guò)程中，數(shù)組的下標(biāo)需要映射為區(qū)間抽象域，對(duì)程序中訪問(wèn)矩陣某個(gè)元素操作采用如下的方式作為該元素的穩(wěn)定上近似，即取下標(biāo)區(qū)間內(nèi)的所有區(qū)間元素的最小上界。假設(shè)數(shù)組行下標(biāo)變量，列下標(biāo)變量，那么有

在程序分析過(guò)程中，訪問(wèn)二維數(shù)組的單個(gè)元素時(shí)取A［i］［j］＝Ai∩iAjr。如果i⊥i或者j⊥i，則Ai，Ajr⊥i，使用前必須先判斷交集是否為⊥i。下面給出針對(duì)C語(yǔ)言程序分析過(guò)程中需要使用到的各種遷移函數(shù)的詳細(xì)設(shè)計(jì)。

賦值遷移函數(shù) （assignment transfer function）

對(duì)于程序中矩陣元素的賦值語(yǔ)句A［i］［j］＝expr在抽象環(huán)境X＃下，程序的狀態(tài)發(fā)生變化，矩陣元素值需要更新，反應(yīng)在區(qū)間向量抽象域中則需要更新區(qū)間向量對(duì)中相應(yīng)的元素，賦值遷移函數(shù)形式化定義如下

其中，［expr］＃X＃表示程序在某程序點(diǎn)對(duì)應(yīng)的抽象環(huán)境X＃下計(jì)算表達(dá)式expr所得到的區(qū)間抽象值。

測(cè)試遷移函數(shù) （test transfer function）

對(duì)于程序中矩陣元素相關(guān)的測(cè)試語(yǔ)句A［i］［j］ test，（其中 ｛≤，≥｝）在不同的測(cè)試分支中，相關(guān)矩陣的狀態(tài)不同，因此，在不同分支中矩陣元素的值范圍需要進(jìn)行相應(yīng)的更新，在抽象域中表現(xiàn)為更新區(qū)間向量對(duì)中相應(yīng)元素的值。

由于抽象環(huán)境X＃中存放該程序點(diǎn)中所有變量的抽象域，因此，此時(shí)的抽象環(huán)境中對(duì)應(yīng)矩陣元素的抽象域表示有X＃（A［i］［j］）＝〈Ai，Ajr〉，其中假設(shè)區(qū)間向量抽象域中相應(yīng)的元素表示為，且有Ai是矩陣相應(yīng)元素值范圍的上近似，test表達(dá)式計(jì)算出的區(qū)間假設(shè)表示為test［c，d］。

那么針對(duì)程序中測(cè)試語(yǔ)句≤和≥分別有式 （12）、式（13）實(shí)現(xiàn)區(qū)間向量抽象域元素狀態(tài)的遷移

上式中各變量在區(qū)間抽象域上的關(guān)系如圖1所示。

圖1 區(qū)間關(guān)系

2 實(shí)驗(yàn)與實(shí)驗(yàn)結(jié)果分析

本文實(shí)驗(yàn)基于開(kāi)源的編譯器前端goto－cc［9］（支持嵌入式C）及開(kāi)源的數(shù)值抽象域庫(kù)Apron［10］，開(kāi)發(fā)了面向嵌入式C數(shù)值程序分析原型工具。

goto－cc是由牛津大學(xué)Daniel等開(kāi)發(fā)的編譯器，用于將嵌入式C程序編譯成控制流圖。本文實(shí)驗(yàn)是在該編譯器生成的控制流圖上利用抽象解釋理論框架求不動(dòng)點(diǎn)實(shí)現(xiàn)對(duì)程序的靜態(tài)分析。

Apron 是由法國(guó)INRIA 開(kāi)發(fā)的一個(gè)開(kāi)源數(shù)值抽象域庫(kù)。為程序分析工具開(kāi)發(fā)者提供一個(gè)通用的抽象域獨(dú)立的接口，可以通過(guò)接口直接使用其中已有的抽象域，還為新抽象域的開(kāi)發(fā)提供通用的設(shè)計(jì)接口。本文的區(qū)間向量抽象域就是基于Apron 庫(kù)提供的接口設(shè)計(jì)和實(shí)現(xiàn)的。

本文實(shí)驗(yàn)基于的環(huán)境是：Ubuntu 10Linux操作系統(tǒng)，2G 物理內(nèi)存，1.70GHZ雙核CPU 處理器。本文抽象域的實(shí)現(xiàn)及與已有方法的對(duì)比實(shí)驗(yàn)均是基于該環(huán)境。

圖2給出一個(gè)從實(shí)際嵌入式C 程序抽取出一個(gè)簡(jiǎn)單的有代表性的矩陣加法的程序片段，為方便精度比較，給二維數(shù)組賦值為簡(jiǎn)單的數(shù)值。并且，在不動(dòng)點(diǎn)迭代時(shí)為了不讓拓寬操作影響各方法分析精度，這里循環(huán)展開(kāi)次數(shù)設(shè)為3次，拓寬延遲1次。

下面對(duì)各主流對(duì)矩陣抽象方法的實(shí)驗(yàn)結(jié)果進(jìn)行比較。Blanche提出將矩陣所有元素抽象為一個(gè)變量方法 （下文簡(jiǎn)稱單變量法），無(wú)法刻畫(huà)元素之間的區(qū)別，無(wú)法描述矩陣元素的有序性，計(jì)算結(jié)果雖是矩陣所有元素的上近似，精度損失很大。侯蘇寧提出將矩陣每個(gè)元素均抽象為一個(gè)變量（下文簡(jiǎn)稱完全展開(kāi)法），精度損失最小，計(jì)算結(jié)果與具體域最接近，但是在實(shí)際程序分析過(guò)程中效率極低，該方法并不實(shí)用。本文區(qū)間向量抽象域能夠較好刻畫(huà)元素之間區(qū)別，在精度損失較小的情況下增加實(shí)用性。上述3種方法對(duì)數(shù)組c實(shí)驗(yàn)結(jié)果如下所示：

圖2 矩陣加法程序片段

單變量法

完全展開(kāi)法

區(qū)間向量法

該程序片段中矩陣加法實(shí)際求解結(jié)果為：｛｛3，9，6，8｝，｛10，7，14，16｝，｛4，6，10，10｝，｛7，14，11，18｝｝根 據(jù) 上 面 的 實(shí)驗(yàn)結(jié)果，可以看出本文的方法能夠穩(wěn)定且較精確的表示矩陣各元素的值范圍。

在空間開(kāi)銷上，單變量法抽象方法簡(jiǎn)單，對(duì)于每個(gè)表示矩陣變量的數(shù)組變量，無(wú)論數(shù)組的長(zhǎng)度是多大均抽象為單個(gè)數(shù)值變量，因此，對(duì)于一個(gè)數(shù)組變量?jī)H需要的一個(gè)抽象值，空間開(kāi)銷復(fù)雜度是一個(gè)常數(shù)O（1）級(jí)。而完全展開(kāi)法對(duì)一個(gè)矩陣中的每個(gè)元素都用一個(gè)抽象值 （區(qū)間）表示，抽象值的空間開(kāi)銷是依據(jù)數(shù)組的元素個(gè)數(shù)而定的。因此，對(duì)一個(gè)有m×n個(gè)數(shù)組元素的矩陣需要的抽象值個(gè)數(shù)為m×n個(gè)，對(duì)每個(gè)抽象值的表示采用的是區(qū)間抽象域那么，空間復(fù)雜度是O（m×n）級(jí)。本文的區(qū)間向量抽象域依據(jù)矩陣的各行、各列分別進(jìn)行區(qū)間抽象，即m 行抽象出一個(gè)含m個(gè)區(qū)間元素的區(qū)間向量，n列抽象出一個(gè)含n 個(gè)區(qū)間元素的區(qū)間向量，需要抽象區(qū)間的開(kāi)銷為m＋n個(gè)，因此空間開(kāi)銷復(fù)雜度為O（m＋n）級(jí)。

在時(shí)間開(kāi)銷上，單變量法在抽象域?qū)仃囘M(jìn)行操作時(shí)只需要對(duì)一個(gè)抽象值進(jìn)行交、接合、拓寬等操作，也不會(huì)因?yàn)榫仃囋氐亩嗌俣兓?，完成一次?duì)矩陣的操作，只需要執(zhí)行域上操作一次。需要時(shí)間自然最少。完全展開(kāi)法則在每次進(jìn)行交、接合、拓寬等操作時(shí)都需要對(duì)m×n個(gè)抽象值（區(qū)間）均進(jìn)行操作，因此，完成一次對(duì)矩陣的操作時(shí)需要進(jìn)行m×n次的域上的操作操作，消耗時(shí)間最大。本文提出的區(qū)間向量抽象域在進(jìn)行交、接合、拓寬等操作時(shí)，僅需要對(duì)m＋n個(gè)區(qū)間抽象值進(jìn)行操作，即完成一次對(duì)矩陣的操作時(shí)需要執(zhí)行域上的操作m＋n次。表1為3種方法比較。

表1 3種方法數(shù)據(jù)比較

實(shí)驗(yàn)結(jié)果表明本文提出的區(qū)間向量抽象域?qū)仃囎兞窟M(jìn)行抽象，在時(shí)空效率以及分析精度作了很好的權(quán)衡。

3 結(jié)束語(yǔ)

本文在經(jīng)典區(qū)間抽象域的基礎(chǔ)上，提出針對(duì)矩陣運(yùn)算的區(qū)間向量抽象域，綜合考慮數(shù)組元素運(yùn)算的精確性以及計(jì)算的效率。將一個(gè)矩陣 （二維數(shù)組）抽象為兩個(gè)區(qū)間向量，將矩陣每一行元素抽象為一個(gè)區(qū)間獲得一個(gè)區(qū)間向量，將矩陣每一列元素也抽象為一個(gè)區(qū)間獲得另一個(gè)區(qū)間向量。在程序中訪問(wèn)某個(gè)元素時(shí)，根據(jù)數(shù)組下標(biāo)，由行號(hào)索引該元素所在行的抽象區(qū)間，由列號(hào)索引該元素所在列的抽象區(qū)間，那么兩個(gè)區(qū)間的交集作為該元素的近似。能夠體現(xiàn)元素之間的差異性且較精確的表示數(shù)組元素，同時(shí)，在時(shí)間和空間消耗上取得合理的權(quán)衡。實(shí)驗(yàn)分析結(jié)果證實(shí)區(qū)間向量抽象域?qū)仃囘\(yùn)算的精確性以及實(shí)用性。

［1］Cousot P.Formal verification by abstract interpretation ［G］.LNCS 7226： NASA Formal Methods. Norfolk， USA：Springer Berlin Heidelberg，2012：3－7.

［2］Gopan D.Numeric program analysis techniques with applications to array analysis and library summarization ［D］.Madison：University of Wisconsin，2007：64－93.

［3］ZHANG Shijin，SHANG Zhaowei.Detection of array bound overflow by interval set based on Cppcheck ［J］.Journal of Computer Applications，2013，33 （11）：3257－3261 （in Chinese）.［張仕金，尚趙偉.基于區(qū)間集的Cppcheck數(shù)組邊界缺陷檢測(cè) ［J］.計(jì)算機(jī)應(yīng)用，2013，33 （11）：3257－3261.］

［4］HOU Suning.Research on value range analysis based on abstract interpretation ［D］.Changsha：National University of Defense Technology，2009 （in Chinese）.［侯蘇寧.基于抽象解釋的數(shù)值程序分析技術(shù)研究 ［D］.長(zhǎng)沙：國(guó)防科學(xué)技術(shù)大學(xué)，2009.］

［5］HOU Suning，CHEN Liqian.A static analyzer for numerical programs in C and Fortran ［J］.Computer Engineering ＆Science，2011，33 （3）：94－102 （in Chinese）.［侯蘇寧，陳立前.一個(gè)面向C和Fortran數(shù)值程序的靜態(tài)分析工具 ［J］.計(jì)算機(jī)工程與科學(xué)，2011，33 （3）：94－102.］

［6］JIANG Jiahong，CHEN Liqian.Floating－point program analysis based on floating－point power set of intervals abstract domain［J］.Journal of Frontiers of Computer Science and Technology，2013，7 （3）：209－217 （in Chinese）.［姜加紅，陳立前.基于浮點(diǎn)區(qū)間冪集抽象域的浮點(diǎn)程序分析 ［J］.計(jì)算機(jī)科學(xué)與探索，2013，7 （3）：209－217.］

［7］WANG Yawen，GONG Yunzhan.A method of variable range analysis based on abstract interpretation and its applications［J］.Chinese of Journal Electronics，2011，39 （2）：296－303（in Chinese）.［王雅文，宮云戰(zhàn).基于抽象解釋的變量值范圍分析及應(yīng)用 ［J］.電子學(xué)報(bào)，2011，39 （2）：296－303.］

［8］ZHANG Jianhua.The global optimization algorithm using interval mathematics and its application research ［D］.Hefei：Hefei University of Technology，2012 （in Chinese）.［張建華.基于區(qū)間數(shù)學(xué)的全局優(yōu)化算法及其應(yīng)用研究 ［D］.合肥：合肥工業(yè)大學(xué)，2012.］

［9］University of Oxford.Goto－cc－a C／C＋＋front－end for Verification ［EB／OL］. ［2014－03－19］.http：／／www.cprover.org／goto－cc.HTM.

［10］Jeannet B，Mine A.The APRON library for numerical abstract domains ［C］／／Proceedings of the 21st International Conference on Computer Aided Verification，2009：661－667.