張弛　黃志球　丁澤文　劉林武

摘要：安全關(guān)鍵領(lǐng)域中，如何保證軟件安全性已經(jīng)成為了一個(gè)廣受關(guān)注的重要課題。確保程序中沒(méi)有運(yùn)行時(shí)錯(cuò)誤，對(duì)于軟件安全性的保證十分重要。基于抽象解釋的靜態(tài)分析方法對(duì)程序語(yǔ)義進(jìn)行抽象，是驗(yàn)證運(yùn)行時(shí)錯(cuò)誤最合適的形式化方法之一?？膳渲贸绦蚍治觯╟onfigurable program analysis，CPA）是一種適合多種靜態(tài)分析方法的通用分析框架。本文使用CPA對(duì)抽象解釋分析方法進(jìn)行建模，給出了使用基于CPA的抽象解釋方法驗(yàn)證程序中的運(yùn)行時(shí)錯(cuò)誤的驗(yàn)證流程，并用實(shí)例說(shuō)明該驗(yàn)證方法的有效性。為程序中運(yùn)行時(shí)錯(cuò)誤的自動(dòng)化分析和驗(yàn)證提供了一種可行方案。

關(guān)鍵詞：可配置程序分析；抽象解釋?zhuān)混o態(tài)分析；運(yùn)行時(shí)錯(cuò)誤驗(yàn)證

中圖分類(lèi)號(hào)：TP311文獻(xiàn)標(biāo)識(shí)碼：A

Abstract：How to ensure software safety has become an important subject in safety critical domain.Ensuring the absence of runtime errors in the program is very important for the safety of the software.The program semantics was abstracted by the static analysis method based on abstract interpretation，and it is one of the most appropriate formal methods for validating runtime errors.Configurable program analysis is a general analytical framework for a variety of static analysis methods.The CPA is used to model the abstraction analysis method，and the validation process of using CPAbased abstract interpretation method to verify the runtime errors in the program is given.Then the effectiveness of the method is illustrated by an example.This provides a feasible solution for the automatic analysis and verification of runtime errors in the program.

Key words：configurable program analysis；abstract interpretation；static analysis；runtime error verification

1引言

近年來(lái)，隨著軟件在醫(yī)療、交通、航空航天等安全關(guān)鍵領(lǐng)域的廣泛應(yīng)用，軟件已經(jīng)成為決定系統(tǒng)安全性的主導(dǎo)因素，如何提高軟件質(zhì)量，保證系統(tǒng)安全性，防止災(zāi)害事故的發(fā)生，已經(jīng)成為當(dāng)前工業(yè)界和學(xué)術(shù)界的重要研究課題[1]。程序作為軟件的核心，對(duì)于程序中運(yùn)行時(shí)錯(cuò)誤的驗(yàn)證是確保軟件安全重要的一環(huán)。運(yùn)行時(shí)錯(cuò)誤是一類(lèi)特定的軟件錯(cuò)誤，是指程序在運(yùn)行時(shí)或運(yùn)行后發(fā)生的錯(cuò)誤，并不是軟件需求和設(shè)計(jì)階段引入的問(wèn)題，而是在程序編寫(xiě)時(shí)，由于違反程序語(yǔ)言的安全性規(guī)范而引入的問(wèn)題[2]。例如程序中出現(xiàn)除數(shù)為零的情況、程序中出現(xiàn)數(shù)組下標(biāo)越界的情況等等。

工業(yè)界常用的仿真、模擬、測(cè)試等手段可以發(fā)現(xiàn)大部分運(yùn)行時(shí)錯(cuò)誤，但卻無(wú)法保證軟件中沒(méi)有運(yùn)行時(shí)錯(cuò)誤[3]。形式化分析與驗(yàn)證方法是保障軟件安全性和可靠性的一種重要方法。學(xué)術(shù)界目前主要使用形式化的靜態(tài)分析方法來(lái)對(duì)運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證。形式化的方法如模型檢測(cè)[4]需要窮舉所有狀態(tài)空間，存在狀態(tài)空間爆炸的問(wèn)題；定理證明[5]需要大量人工參與，難以自動(dòng)化。抽象解釋對(duì)程序語(yǔ)義進(jìn)行抽象，將程序的具體語(yǔ)義轉(zhuǎn)化到抽象域中對(duì)程序的性質(zhì)進(jìn)行分析[6]。其根據(jù)需求對(duì)程序語(yǔ)義進(jìn)行近似，調(diào)節(jié)靜態(tài)分析的精度和效率，是目前對(duì)運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證的主要方法。

可配置程序分析是一個(gè)形式化的進(jìn)行軟件驗(yàn)證和程序分析的通用框架。旨在用一種通用的形式化體系，通過(guò)配置不同的參數(shù)，來(lái)設(shè)計(jì)實(shí)現(xiàn)多種靜態(tài)分析方法[7]。因此可以使用基于CPA的靜態(tài)分析框架來(lái)對(duì)抽象解釋的分析階段進(jìn)行建模。來(lái)對(duì)運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證。

本文第2節(jié)簡(jiǎn)單介紹抽象解釋中的基本概念和用于之后分析的區(qū)間抽象域。第3節(jié)具體介紹CPA靜態(tài)分析框架的形式化體系表示方法及相應(yīng)的迭代算法。第4節(jié)給出運(yùn)行時(shí)錯(cuò)誤的具體驗(yàn)證流程。第5節(jié)用一個(gè)實(shí)例來(lái)解釋說(shuō)明如何使用該方法，來(lái)對(duì)程序中的運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證。第6節(jié)，結(jié)束語(yǔ)。

2相關(guān)理論

21基于格的抽象解釋

抽象解釋理論是P.Cousot和R.Cousot于1977年提出的對(duì)程序語(yǔ)義進(jìn)行可靠近似理論[8][9]。其基本思想是用抽象語(yǔ)義代替具體語(yǔ)義來(lái)描述源程序語(yǔ)言，利用得到的抽象語(yǔ)義來(lái)實(shí)現(xiàn)具體語(yǔ)義的計(jì)算，程序的抽象執(zhí)行的結(jié)果能反映程序真實(shí)執(zhí)行的部分信息。抽象解釋本質(zhì)上是一種基于格的程序分析方法，下面給出一些相關(guān)的基礎(chǔ)概念。

定義2.1偏序：如果≤是p上的二元關(guān)系，如果p中所有元素都具有自反性、傳遞性和反對(duì)稱(chēng)性，則稱(chēng)≤為p上的偏序關(guān)系，稱(chēng)為一個(gè)（p，≤）偏序集。

定義2.2格：對(duì)于偏序集（P，≤），若P中任意兩個(gè)元素都存在上確界和下確界，則稱(chēng)（P，≤）是格，為方便，這樣的格稱(chēng)為偏序格。

定義2.3完備格：對(duì)于格（P，≤）如果存在最小元素和最大元素，則稱(chēng)其為完備格，完備格可以用一個(gè)六元組來(lái)（P，≤，∪，∩，⊥，T）表示，其中∪表示最小上屆，∩表示最大下界，⊥表示集合P中最小元，T表示集合P中最大元。

定義2.4伽羅瓦（Galois）連接[10]：如果兩個(gè)偏序集（P，≤）和（P*，≤*）之間存在轉(zhuǎn)化函數(shù)α：P→P*和逆向轉(zhuǎn)化函數(shù)Y：P*→P，當(dāng)對(duì)x∈P，x*∈P*，α（x）≤*x*x≤γ（x*）則稱(chēng)轉(zhuǎn)化函數(shù)構(gòu)成的函數(shù)對(duì)（α，γ）為集合P和P*之間的伽羅瓦連接，記作：

（P，≤）αγ（P*，≤*）

其中，稱(chēng)（P，≤）為具體域，（P*，≤*）為抽象域，轉(zhuǎn)化函數(shù)α為抽象函數(shù)，轉(zhuǎn)化函數(shù)γ為具體函數(shù)。

22區(qū)間抽象域

區(qū)間抽象域在靜態(tài)分析過(guò)程中，主要用于表示某程序點(diǎn)處某一變量可能取到的最小值和最大值所構(gòu)成的區(qū)間來(lái)近似[11]。具體域和抽象域之間的關(guān)系可以通過(guò)下面一個(gè)Galois連接來(lái)表示：

（R，≤）αγ（Itvs，i）

區(qū)間抽象域可以用一個(gè)完備格來(lái)表示，即（Itvs，i，∪i，∩i，⊥i，Ti），其中，Itvs是實(shí)數(shù)R上的區(qū)間的集合，其形式化的表示為：

{[a，b]|a∈R∪{-∞}，b∈R∪{+∞}，a≤b}∪{⊥i}。

i是Itvs上的偏序關(guān)系，形式化定義為：[a，b]i[a′，b′]當(dāng)且僅當(dāng)[a，b]=⊥i或者a≥a′^b≤b′，⊥i為集合上的最小元，滿足γ（⊥i）Δ，（-∞，+∞）為集合上的最大元，滿足對(duì)I∈Itvs，Ii[-∞，+∞]。通過(guò)這樣的方式可以將程序中變量的取值抽象成形如a≤x≤b的約束，可以用于與分析變量取值范圍相關(guān)的程序?qū)傩则?yàn)證，例如除零錯(cuò)或數(shù)組越界的驗(yàn)證。"

3基于CPA的抽象解釋分析方法

CPA是一個(gè)形式化的軟件驗(yàn)證和程序分析的通用框架，可以通過(guò)配置參數(shù)來(lái)實(shí)現(xiàn)不同靜態(tài)分析方法?；贑PA的抽象解釋靜態(tài)分析方法以程序控制流圖為分析對(duì)象，選擇不同抽象精度的抽象域來(lái)決定分析過(guò)程的抽象層次，選擇不同的merge操作和stop操作來(lái)配置不同的迭代分析算法。其配置分析過(guò)程如圖1所示。

在CPA配置分析過(guò)程中，將程序控制流圖信息結(jié)合抽象域的定義，得到抽象狀態(tài)的遷移關(guān)系；根據(jù)抽象域中域操作的定義配置CPA迭代算法中的merge操作和stop操作。根據(jù)抽象狀態(tài)的遷移關(guān)系，執(zhí)行CPA迭代算法來(lái)求解不動(dòng)點(diǎn)抽象值，抽象狀態(tài)之間通過(guò)merge操作來(lái)合并形成新的抽象狀態(tài)，直至stop操作為真，則可判斷沒(méi)有新的抽象狀態(tài)產(chǎn)生，迭代結(jié)束。

下面介紹CPA的形式化體系的表示方法和相應(yīng)的CPA迭代算法。

31CPA形式化體系

CPA形式化定義為ID=（D，∽，merge，stop）， 其中包括抽象域D，抽象狀態(tài)遷移關(guān)系∽，合并操作merge，終止判斷操作stop。 CPA通過(guò)配置這四部分來(lái)完成一次靜態(tài)分析的分析階段，通過(guò)選擇不同的配置來(lái)實(shí)現(xiàn)不同精度和效率的靜態(tài)分析。下面具體說(shuō)明這四部分

（1）抽象域D=（C，ε，[·]），其中C為程序具體狀態(tài)的集合，其中一個(gè)具體狀態(tài)c為程序運(yùn)行到某一狀態(tài)時(shí)變量在不同程序結(jié)點(diǎn)處的實(shí)際值，即X∪{Pc}，其中X為變量集合，{Pc}為程序結(jié)點(diǎn)集合。ε是用于描述抽象環(huán)境的完備格ε=（E，，∩，∪，⊥，T），其中E是抽象狀態(tài)集合，E×E是抽象狀態(tài)間的偏序關(guān)系，∩表示最大下界，∪表示最小上界，⊥∈E表示集合中的最小元素，T∈E 表示集合中的最大元素。具體化方法[·]：E→2c賦予抽象狀態(tài)其對(duì)應(yīng)的具體狀態(tài)集，即一個(gè)抽象狀態(tài)可能對(duì)應(yīng)多個(gè)具體狀態(tài)。為了保證分析可靠性（soundness），我們要求[T]=C，[⊥]=；e，e′∈E，[e∪e′][e]∪[e′]。

（2）抽象狀態(tài)遷移∽E×G×E其中E是抽象狀態(tài)集合，G是控制流圖的邊的集合?！妆硎疽粋€(gè)抽象狀態(tài)e通過(guò)一個(gè)CFG的邊g到達(dá)一個(gè)新的抽象狀態(tài)e′記為e∽e′。為了保證分析過(guò)程的可靠性，我們要求e∈E：e′∈E：e∽e′，e∈E，g∈G：Uegete′[e′]UC∈[e]{C′|CgC′}。

（3）合并操作符merge：E×E→E將兩個(gè)抽象狀態(tài)的信息進(jìn)行合并。為了保證分析的可靠性，我們要求

e′merge（e，e′）。

（4）終止判斷操作stop：E×2E→B表示某一個(gè)抽象狀態(tài)是否被一個(gè)抽象狀態(tài)集合所覆蓋，為了保證分析的可靠性，我們要求

stop（e，R）=true→[e]∪e′∈R[e′]。

32CPA迭代算法

CPA的迭代算法是可達(dá)性計(jì)算算法。其輸入為一組配置完成的CPAID=（D，∽，merge，stop），以及一個(gè)初始抽象狀態(tài)e0∈E，其中E是抽象域D中的抽象狀態(tài)的集合。CPA執(zhí)行算法不斷更新兩個(gè)存放抽象狀態(tài)的集合。一個(gè)是reached集合，用來(lái)存放所有可以到達(dá)的抽象狀態(tài)。一個(gè)是waitlist集合，用來(lái)存放所有還未被執(zhí)行過(guò)的抽象狀態(tài)。對(duì)于某一狀態(tài)e，根據(jù)抽象狀態(tài)遷移關(guān)系∽可以找到其對(duì)應(yīng)的一個(gè)或多個(gè)后繼結(jié)點(diǎn)，對(duì)于任意后繼結(jié)點(diǎn)e′，用其與目前reached集合中所有的抽象狀態(tài)進(jìn)行merge操作。然后判斷是否有新的結(jié)點(diǎn)產(chǎn)生，即是否沒(méi)有被reached集合中所有抽象狀態(tài)所覆蓋。如果產(chǎn)生新的抽象狀態(tài)，則將其加入reached集合和waitlist集合中。重復(fù)執(zhí)行算法，直至所有的抽象狀態(tài)進(jìn)行merge操作后都無(wú)法找到新的結(jié)點(diǎn)，即此時(shí)找到的程序的不動(dòng)點(diǎn)。具體的執(zhí)行算法流程詳見(jiàn)表1。

4程序運(yùn)行時(shí)錯(cuò)誤的驗(yàn)證方法

圖2給出了一個(gè)基于CPA的抽象解釋方法的分析框架，用于對(duì)程序的運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證。該過(guò)程主要分為三個(gè)階段：預(yù)處理階段、分析階段和驗(yàn)證階段。

在預(yù)處理階段。由于抽象解釋方法是一個(gè)基于狀態(tài)遷移系統(tǒng)的分析方法，因此需要在預(yù)處理階段，將待分析系統(tǒng)轉(zhuǎn)化成與之等價(jià)的抽象表示，即通過(guò)詞法分析和語(yǔ)法分析器得到其抽象語(yǔ)法樹(shù)，然后轉(zhuǎn)化成便于進(jìn)行分析的狀態(tài)遷移系統(tǒng)。之后，我們將狀態(tài)遷移系統(tǒng)轉(zhuǎn)化到程序控制流圖（control-flow graph，CFG）[12]。

分析階段是抽象解釋理論表現(xiàn)的主要階段。在這個(gè)階段，CPA靜態(tài)分析框架需要以程序控制流圖、抽象域的域元素、配置的merge操作和配置的stop操作為輸入。其中程序控制流圖由預(yù)處理階段生成。其中抽象域中的域元素以完備格的形式提供輸入，在相應(yīng)的域操作中提取merge操作和stop操作，以完成CPA形式化體系的輸入。相應(yīng)的CPA迭代算法運(yùn)用抽象解釋中的迭代策略，計(jì)算程序控制流圖中所有結(jié)點(diǎn)的不動(dòng)點(diǎn)抽象值，從而完成分析。

在驗(yàn)證階段，將得到的程序結(jié)點(diǎn)上的不動(dòng)點(diǎn)抽象值轉(zhuǎn)化為程序具體的變量約束關(guān)系，根據(jù)系統(tǒng)的需求文檔和設(shè)計(jì)說(shuō)明文檔對(duì)程序的變量數(shù)值性質(zhì)進(jìn)行分析，判斷變量的數(shù)值性質(zhì)是否滿足規(guī)約，得到分析結(jié)果，從而完成整個(gè)抽象解釋靜態(tài)分析的過(guò)程。圖3以除零錯(cuò)為例，說(shuō)明如何對(duì)運(yùn)行時(shí)錯(cuò)誤進(jìn)行驗(yàn)證。根據(jù)分析階段得到的不動(dòng)點(diǎn)抽象值，結(jié)合源程序中與除數(shù)變量相關(guān)的代碼，得到變量的約束關(guān)系，然后判斷在各個(gè)程序結(jié)點(diǎn)，是否存在除數(shù)為零的情況，完成分析驗(yàn)證。

4CPA的分析實(shí)例

本章用一個(gè)實(shí)例來(lái)說(shuō)明如何使用可配置程序分析CPA來(lái)對(duì)基于抽象解釋的靜態(tài)分析的分析階段進(jìn)行建模。以圖4中代碼為例，使用區(qū)間抽象域進(jìn)行分析，以期得到各個(gè)程序結(jié)點(diǎn)處變量的取值范圍。

根據(jù)第四章分析框架，首先在預(yù)處理階段，根據(jù)相關(guān)詞法分析和語(yǔ)法分析，將源程序轉(zhuǎn)化到其控制流圖，轉(zhuǎn)化結(jié)果如圖5所示。

在分析階段，根據(jù)程序控制流圖和抽象域的定義，配置CPAID=（D，∽，merge，stop），即分別配置抽象域D，抽象狀態(tài)遷移關(guān)系∽，抽象狀態(tài)的合并操作merge，終止判斷操作stop。下面給出具體過(guò)程：

（1）配置抽象域D=（C，ε，[·]）為區(qū)間抽象域。其中C為程序具體狀態(tài)的集合C{pc，x}，其中pc∈{s1，s2，…，s11}，X={x，y}；描述抽象環(huán)境的完備格

ε=（E，，∩，∪，⊥，T），其中E是抽象狀態(tài)集合，具體狀態(tài)和抽象狀態(tài)通過(guò)一個(gè)Galois連接彼此關(guān)聯(lián)

（R，≤）αγ（Itvs，）

其中R是實(shí)數(shù)域，Itvs是實(shí)數(shù)域上的區(qū)間集合。例如程序具體狀態(tài)c（pc=s3，{x=0，y=0}）轉(zhuǎn)化成的抽象狀態(tài)是e（pc=s3，{x∈[0，0]，y∈[0，0]}）。

（2）抽象狀態(tài)遷移關(guān)系∽，一個(gè)抽象狀態(tài)通過(guò)圖2程序控制流圖上連通的一邊到達(dá)一個(gè)新的狀態(tài)。例如抽象狀態(tài)e（pc=c，i∈[1，1]）通過(guò)邊（pc=c，i=i+1，pc′=d）到達(dá)抽象狀態(tài)e′（pc=d，i∈[2，2]）；抽象狀態(tài)e（pc=c，i∈[1，11]通過(guò)邊（pc=b，assume（i<=10），pc′=c）到達(dá)抽象狀態(tài)e′（pc=c，i∈[1，10]）。以此類(lèi)推來(lái)遍歷尋找所有可能達(dá)到的抽象狀態(tài)。

（3）合并操作符merge用以表示兩個(gè)抽象狀態(tài)的合并，在經(jīng)典區(qū)間抽象域的抽象解釋中，表示兩個(gè)區(qū)間抽象域的合并，即mergejoin（e，e′）=e∪e′。

兩個(gè)區(qū)間的合并如下：

例如抽象狀態(tài)e（pc=s3，{x∈[0，0]，y∈[0，0]}）與抽象狀態(tài)

e′（pc=s3，{x∈[1，1]，y∈[1，1]}）進(jìn)行merge操作形成新的新的抽象狀態(tài)

e″（pc=s3，{x∈[0，1]，y∈[0，1]}）。

（4）終止判斷操作stop用以判斷某一個(gè)抽象狀態(tài)是否被一個(gè)抽象狀態(tài)集合所覆蓋，在區(qū)間抽象域的抽象解釋中表示是否產(chǎn)生了之前所達(dá)到的抽象狀態(tài)集合沒(méi)有覆蓋到的抽象狀態(tài)，即程序是否到達(dá)了不動(dòng)點(diǎn)，如果經(jīng)過(guò)所有的遷移關(guān)系，都沒(méi)有新抽象狀態(tài)的產(chǎn)生，則整個(gè)抽象解釋的分析就到達(dá)不動(dòng)點(diǎn)。其配置為

stopjoin（e，R）=e∪e′∈Re′。

在完成配置CPA之后，執(zhí)行CPA迭代算法。算法輸入ID=（D，∽，merge，stop），初始狀態(tài)

e0=（pc=s1，{x=⊥，y=⊥}），經(jīng)過(guò)表1的CPA的迭代算法之后，各個(gè)程序結(jié)點(diǎn)處的不動(dòng)點(diǎn)抽象值如表2所示：

根據(jù)算法結(jié)果，得到變量x和變量y在全部程序結(jié)點(diǎn)處的取值范圍，可以對(duì)一些變量數(shù)值相關(guān)的運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證。證明了該分析方法的有效性和可行性。

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

針對(duì)程序中的運(yùn)行時(shí)錯(cuò)誤，本文提出了一種基于CPA的抽象解釋的分析方法。首先介紹了一種支持抽象解釋的靜態(tài)分析框架，即可配置程序分析；然后給出了具體的靜態(tài)分析流程，如何從源程序出發(fā)，轉(zhuǎn)化成與之等價(jià)的控制流圖，再轉(zhuǎn)化到CPA形式化體系中進(jìn)行迭代計(jì)算，最后根據(jù)得到的不動(dòng)點(diǎn)抽象值進(jìn)行相關(guān)運(yùn)行時(shí)錯(cuò)誤的分析驗(yàn)證；最后給出一個(gè)實(shí)例的分析過(guò)程，說(shuō)明該靜態(tài)分析方法的可行性和有效性。

接下來(lái)的工作中，我們將進(jìn)一步擴(kuò)展CPA支持的抽象域，如八邊形抽象域、多面體抽象域，甚至一些非凸抽象域。并給出一個(gè)自動(dòng)化的對(duì)運(yùn)行時(shí)錯(cuò)誤進(jìn)行分析和驗(yàn)證的工具，來(lái)對(duì)研究工作進(jìn)行完善。

參考文獻(xiàn)

[1]黃志球，徐丙鳳，闞雙龍，等.嵌入式機(jī)載軟件安全性分析標(biāo)準(zhǔn)、方法及工具研究綜述[J].軟件學(xué)報(bào)，2014，25（2）：200-218.

[2]DELMAS D，SOUYRIS J.Astrée：from research to industry[C]//International Static Analysis Symposium.Springer Berlin Heidelberg，2007：437-451.

[3]計(jì)算機(jī)科學(xué)技術(shù)百科全書(shū) ：選編本[M].北京：清華大學(xué)出版社，2002.

[4]CLARK E M，GRUMBERG O，PELED D.Model checking[M].MIT press，1999.

[5]L Hai，S Jigui，Z Yimin.Theorem Proving Based on the Extension Rule.[J].Journal of Automated Reasoning，2003，31（1）：11-21.

[6]COUSOT P，COUSOT R.Basic concepts of abstract interpretation[M]//Building the Information Society.Springer US，2004：359-366.

[7]BEYER D，HENZINGER T A，Théoduloz G.Configurable Software Verification：Concretizing the Convergence of Model Checking and Program Analysis[C]// International Conference on Computer Aided Verification.2007：504-518.

[8]COUSOT P，COUSOT R.Abstract Interpretation：A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.[C]// ACM SigactSigplan Symposium on Principles of Programming Languages.1977：238-252.

[9]COUSOT P，COUSOT R，F(xiàn)eret J，et al.The ASTRE Analyzer[J].Lecture Notes in Computer Science，2005，3444：140-140.

[10]COUSOT P，COUSOT R.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[C]// Programming Language Implementation and Logic Programming，International Symposium，Plilp92，Leuven，Belgium，August 26-28，1992，Proceedings.1992：269-295.

[11]COUSOT P，COUSOT R.Static determination of dynamic properties of programs[J].Proceedings of the Second International Symposium on Programming，1976.

[12]HARROLD M J，MALLOY B，ROTHERMEL G.Efficient Construction of Program Dependence Graphs[J].Acm Sigsoft Software Engineering Notes，2000，18（3）：160-170.