高婉玲，趙鶴

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都 610065）

靜態(tài)程序分析方法和工具

高婉玲，趙鶴

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都 610065）

綜述靜態(tài)程序分析的方法和工具。采用系統(tǒng)化文獻(xiàn)評(píng)價(jià)方法和文獻(xiàn)計(jì)量分析方法，通過論文的收集、篩選、內(nèi)容提取等過程，對(duì)大量論文的信息進(jìn)行總結(jié)分析。通過文獻(xiàn)管理工具Endnote、數(shù)據(jù)分析軟件SPSS和文獻(xiàn)分析工具RefViz，統(tǒng)計(jì)分析論文數(shù)據(jù)庫的基本信息，包括年代分布、作者分布、關(guān)鍵詞和熱點(diǎn)分析。通過閱讀大量相關(guān)論文，靜態(tài)程序分析方法可分為模型檢測(cè)、符號(hào)執(zhí)行、定理證明、抽象解釋等。靜態(tài)程序分析工具包括形式化驗(yàn)證工具、模型檢測(cè)工具等。最后，總結(jié)靜態(tài)分析方法和工具的不足。

程序分析；靜態(tài)分析方法；靜態(tài)分析工具；系統(tǒng)化文獻(xiàn)評(píng)價(jià)

0 引言

（1）研究背景

程序分析是計(jì)算機(jī)科學(xué)與技術(shù)領(lǐng)域的經(jīng)典和核心內(nèi)容，主要是對(duì)某種語言編寫的程序的內(nèi)部流程進(jìn)行分析[1]。根據(jù)程序是否需要運(yùn)行，分為靜態(tài)程序分析與動(dòng)態(tài)程序分析。靜態(tài)程序分析（Static Program Analysis）是在不運(yùn)行代碼的條件下，通過某些分析技術(shù)掃描程序，驗(yàn)證程序是否滿足某些性質(zhì)。動(dòng)態(tài)程序分析（Dynamic Program Analysis）是在真實(shí)環(huán)境或模擬環(huán)境中執(zhí)行程序進(jìn)行分析。靜態(tài)分析方法和工具對(duì)提高軟件的質(zhì)量非常有幫助，所以得到越來越多的重視。本文對(duì)近10年來靜態(tài)程序分析領(lǐng)域的研究現(xiàn)狀進(jìn)行了總結(jié)，綜述了部分靜態(tài)程序分析的方法和工具，總結(jié)了靜態(tài)程序分析的不足，可為研究領(lǐng)域的學(xué)者提供綜合性的參考。

靜態(tài)分析和動(dòng)態(tài)分析的過程[2]如圖1。

（2）研究方法

采用系統(tǒng)性文獻(xiàn)評(píng)價(jià)方法[3]，對(duì)有關(guān)靜態(tài)程序分析的綜述，其步驟如下：

①研究問題

問題1：靜態(tài)程序分析的方法有哪些？

問題2：采用靜態(tài)程序分析方法的工具有哪些？

問題3：靜態(tài)程序分析中有哪些未解決的問題？

圖1 靜態(tài)分析和動(dòng)態(tài)分析過程圖

②搜索策略

以static software analysis、model checking、formal verification、static program analysis、靜態(tài)程序分析及其組合為關(guān)鍵詞，在數(shù)據(jù)庫、會(huì)議論文集中進(jìn)行檢索，年限為2004年至2016年。共搜集篇數(shù)1604篇，其中394篇用于文獻(xiàn)計(jì)量分析，最終采用17篇用于文獻(xiàn)綜述。

③篩選方案

長文優(yōu)于短文；博士學(xué)位論文；EI或SCI期刊；國內(nèi)和國外國際會(huì)議論文。

④數(shù)據(jù)提取和分析對(duì)于檢索到的有關(guān)靜態(tài)程序分析的論文，根據(jù)需要解決的問題對(duì)論文進(jìn)行分類和總結(jié)。

④完成報(bào)告

在完成上述工作的基礎(chǔ)上，完成論文的編寫。

1 文獻(xiàn)計(jì)量分析結(jié)果

1.1 年代分布

圖2 Endnote年代統(tǒng)計(jì)分布圖

通過Endnote工具分析，文獻(xiàn)的年代分布和趨勢(shì)如圖2。該領(lǐng)域直到2011年文獻(xiàn)呈現(xiàn)遞增趨勢(shì)，大致可分為四個(gè)階段：2007年之前為起步階段，2007年-2011年為高速增長階段，2011年-2013年下降趨勢(shì)明顯，2013年之后文章數(shù)量平穩(wěn)上升。

1.2 作者分布

采用SPSS分析作者在該領(lǐng)域內(nèi)發(fā)表論文數(shù)占總體篇數(shù)的頻率（見圖3），每種顏色代表一個(gè)作者，顏色的寬度表示了其發(fā)表的文章的頻率，寬度越寬，則文章數(shù)量越多。

結(jié)論：近年來編寫該領(lǐng)域相關(guān)文獻(xiàn)的作者較多，但是產(chǎn)量都不是很大，高產(chǎn)作者較少。

圖3 SPSS作者統(tǒng)計(jì)圖

1.3 關(guān)鍵詞和熱點(diǎn)分析

RefViz工具中的Matrix視圖（見圖4）是關(guān)鍵詞相似性排列后生成的圖形，橫、縱坐標(biāo)軸上表示的關(guān)鍵詞距離越近，表示關(guān)鍵詞之間的相似度越高，坐標(biāo)軸交匯點(diǎn)紅色越深，代表含有橫、縱坐標(biāo)對(duì)應(yīng)的關(guān)鍵詞的文獻(xiàn)越多。

圖4 Matrix視圖

結(jié)論：RefViz分析結(jié)果顯示文獻(xiàn)一級(jí)關(guān)鍵詞為：software、analysis、technique、model、program、method等，它們是與文章關(guān)聯(lián)性最強(qiáng)的關(guān)鍵詞。RefViz揭示的文獻(xiàn)的熱點(diǎn)為：software、verfication、program、static等。

2 靜態(tài)程序分析方法

2.1 形式化驗(yàn)證（Formal Verification）基本概念

形式化驗(yàn)證采用數(shù)學(xué)方法證明某些形式的規(guī)范或?qū)傩缘恼_性。模型檢測(cè)、符號(hào)執(zhí)行、定理證明、約束求解等多種程序分析方法都屬于形式化驗(yàn)證技術(shù)。近年來形式化驗(yàn)證技術(shù)已經(jīng)有了顯著的提高和進(jìn)步，但驗(yàn)證過程的低可預(yù)測(cè)性、缺乏顯示驗(yàn)證進(jìn)展的指標(biāo)等因素，阻礙了形式化驗(yàn)證成為主流驗(yàn)證技術(shù)[4]。

2.2 模型檢測(cè)（Model Checking）

模型檢測(cè)是檢測(cè)給定結(jié)構(gòu)是否符合給定的邏輯公式的技術(shù)，是一種很重要的自動(dòng)驗(yàn)證技術(shù)[5]。首先要對(duì)有限狀態(tài)的系統(tǒng)構(gòu)造狀態(tài)機(jī)或有向圖等模型，再通過遍歷模型來驗(yàn)證系統(tǒng)的性質(zhì)。模型檢測(cè)成功應(yīng)用于協(xié)議驗(yàn)證和硬件檢測(cè)方面，由于軟件自身的復(fù)雜度，軟件模型檢測(cè)只檢測(cè)抽象模型[6-7]。

模型檢測(cè)技術(shù)存在兩大問題：建模和狀態(tài)空間爆炸。由于抽象模型與實(shí)際系統(tǒng)存在差異，在驗(yàn)證模型的過程中找到的漏洞不一定與代碼中真正的錯(cuò)誤一致。解決建模問題，可以結(jié)合模型檢測(cè)和軟件測(cè)試各自的優(yōu)勢(shì)[5]。針對(duì)狀態(tài)爆炸的問題，符號(hào)化模型檢測(cè)（Symbolic Model Checking）和有界模型檢測(cè)（Bounded Model Checking，BMC）可以有效緩解。將兩者交叉存取的技術(shù)，可以在有限的存儲(chǔ)空間和時(shí)間中，不需要存儲(chǔ)全部可達(dá)狀態(tài)，即可有效地探索狀態(tài)空間[8]。

2.3 符號(hào)執(zhí)行（Symbolic Execution）

符號(hào)執(zhí)行中采用抽象符號(hào)代表變量的值來模擬程序的執(zhí)行過程。優(yōu)點(diǎn)是能夠精確地模擬程序執(zhí)行過程，缺點(diǎn)是不能處理指針對(duì)象及代碼中的循環(huán)。符號(hào)執(zhí)行與約束求解方法相結(jié)合，是一種精確的判定方法。約束條件的集合和求解的能力決定了約束求解工具分析和發(fā)現(xiàn)錯(cuò)誤的效率。如果有足夠的時(shí)間和空間資源，上述方法可以正確判定路徑是否可行[9]。但如果需要枚舉所有可能的路徑，路徑個(gè)數(shù)會(huì)隨程序規(guī)模的增大呈指數(shù)級(jí)增長，出現(xiàn)狀態(tài)爆炸的問題[6]。

2.4 定理證明（Theorem Proving）

定理證明是程序驗(yàn)證中經(jīng)常用到的一種基于語義的分析方法[2，6]。它將驗(yàn)證的問題轉(zhuǎn)換為數(shù)學(xué)問題,來分析程序的指定屬性是否滿足，所以它比很多分析方法復(fù)雜但更準(zhǔn)確。定理證明適用于靜態(tài)代碼，缺點(diǎn)是程序員的工作增多，而且這種驗(yàn)證方法難以應(yīng)用于大規(guī)模程序。目前此方向研究較熱門的是基于邏輯推理自動(dòng)證明程序的性質(zhì)，但由于自動(dòng)化的定理證明難度系數(shù)太大，所以還沒有產(chǎn)品可供工業(yè)界使用。

2.5 抽象解釋（Abstract Interpretation）

抽象解釋由P.Cousot和R.Cousot提出，原理是采用可靠近似分析方法對(duì)數(shù)學(xué)模型進(jìn)行分析，并為不同的近似分析方法創(chuàng)建統(tǒng)一的形式化框架。抽象解釋本質(zhì)上是在計(jì)算效率和精度之間取得均衡，通過不斷迭代，抽象解釋最終為程序建立抽象模型[2]，分析結(jié)果可能不夠精確。抽象解釋的思想和方法在各類編譯器技術(shù)中得到廣泛使用，它的應(yīng)用范圍不僅包括程序分析，還包括程序的調(diào)試、變換等。

2.6 其他程序分析技術(shù)

●類型推導(dǎo)（Type Inference）是自動(dòng)推導(dǎo)變量和函數(shù)類型，適用于控制流無關(guān)的分析，可用于處理大規(guī)模程序，但是分析結(jié)果可能不夠精確。

●實(shí)驗(yàn)程序分析方法（Experimental Program Analysis）[10]是執(zhí)行目標(biāo)程序過程中，在控制條件下，描述或解釋對(duì)一個(gè)或多個(gè)程序的一個(gè)方面的獨(dú)立變量的影響,是一種新形式的程序分析方法。

●靜動(dòng)態(tài)結(jié)合的混合分析技術(shù)結(jié)合了靜態(tài)分析和動(dòng)態(tài)分析的優(yōu)點(diǎn)，可以提高分析結(jié)果的精度，同時(shí)降低了開銷，提高了效率。主要包括兩個(gè)步驟，第一步是將預(yù)處理后的程序與靜態(tài)掃描字節(jié)碼后的結(jié)果進(jìn)行靜態(tài)分析，第二步是對(duì)靜態(tài)分析結(jié)果中不確定的部分進(jìn)行動(dòng)態(tài)分析，將動(dòng)態(tài)分析和靜態(tài)分析的結(jié)果結(jié)合，得到最終的分析結(jié)果[11]。

2.7 靜態(tài)程序分析方法比較

模型檢測(cè)、符號(hào)執(zhí)行、定理證明等與形式化驗(yàn)證相關(guān)緊密，屬于形式化驗(yàn)證方法。模型檢測(cè)、定理證明的分析對(duì)象及處理方法不同：模型檢測(cè)盡可能枚舉所有狀態(tài)，而定理證明是將問題轉(zhuǎn)化為數(shù)學(xué)公式，采用邏輯規(guī)則推導(dǎo)證明。模型檢測(cè)、類型推導(dǎo)是從不同的角度抽象程序：模型檢測(cè)將程序抽象為模型，類型推導(dǎo)將程序抽象為變量或函數(shù)集合。符號(hào)執(zhí)行、類型推導(dǎo)都依賴約束，但是形成約束的方法和約束的表現(xiàn)形式不同：類型推導(dǎo)的約束是一組集合關(guān)系表達(dá)式，符號(hào)執(zhí)行的約束是一組以布爾表達(dá)式、線性等式和不等式。符號(hào)執(zhí)行、約束求解共同的優(yōu)點(diǎn)：對(duì)程序的執(zhí)行可以進(jìn)行精確的模擬。類型推導(dǎo)和抽象解釋共同的缺點(diǎn)：分析結(jié)果都不夠精確。定理證明是非常準(zhǔn)確的，但是方法比較難，而且很難用于大規(guī)模程序。

3 靜態(tài)程序分析工具

靜態(tài)分析工具主要檢查源代碼中的變量、模塊接口的一致性、邏輯上可能存在的錯(cuò)誤結(jié)構(gòu)和不可達(dá)的程序段等[12]。使用靜態(tài)分析工具可以盡早發(fā)現(xiàn)程序錯(cuò)誤，而且有助于發(fā)現(xiàn)編程人員的編碼風(fēng)格的問題。

3.1 形式化驗(yàn)證工具

●FindBugs工具，Java的著名現(xiàn)代工具，有警告提醒、錯(cuò)誤檢測(cè)的功能。在運(yùn)行的過程中，將遍歷并分析所有指定文件，最后將分析結(jié)果可視化。

●lint工具，在C程序中查找簡單錯(cuò)誤。lint和FindBugs的缺點(diǎn)是不能嚴(yán)格保證分析結(jié)果的正確性[13]。

●CODESONAR工具，是使用過程間分析方法來檢查C或C++代碼中模板錯(cuò)誤的工具，檢測(cè)范圍包括緩沖區(qū)溢出、內(nèi)存泄漏、冗余環(huán)路和分支條件。

●K7工具，來自KlocWork公司，可以處理由C、C++與Java組成的復(fù)合的應(yīng)用程序，與CODESONAR工具有類似特點(diǎn)。

●Coverity prevent工具，是靜態(tài)代碼分析工具，被用來在開源項(xiàng)目中查找缺陷。它支持增式分析，可以識(shí)別死鎖、空指針、未初始化變量、緩沖區(qū)溢出等問題。

●SVT(System Verification Test)，靜態(tài)驗(yàn)證工具，模擬用戶可能遇到的測(cè)試場(chǎng)景，以此分析可能的問題或錯(cuò)誤，可以驗(yàn)證由UML類圖和狀態(tài)機(jī)圖組成的UML模型。

●cprover工具，是一個(gè)插件，可以在C程序中進(jìn)行可視化調(diào)試、錯(cuò)誤跟蹤，還具有后臺(tái)驗(yàn)證功能。

3.2 模型檢測(cè)工具

有界模型檢測(cè)工具（BMC）的代表性工具是CBMC，支持C++、SpecC和SystemC語言，它主要檢測(cè)C或SystemC中系統(tǒng)級(jí)的環(huán)路模型與Verilog提供的模板是否一致，并且可以檢測(cè)C程序中斷驅(qū)動(dòng)程序中的數(shù)據(jù)競(jìng)爭(zhēng)[13]。其他還有為特定屬性量身定做的Saturn工具、專門捕獲缺陷的EXE工具、Calysto模型檢測(cè)器和可解決C程序函數(shù)指針問題的VARVEL工具。BMC是尋找淺層缺陷的最好技術(shù)，一旦發(fā)現(xiàn)缺陷，它會(huì)提供一個(gè)完整的反例路徑，但是BMC只能分析簡單的不包含深層循環(huán)的程序[7]；基于執(zhí)行的工具有Verisoft、Java-PathFinder、CMC、MaceMC、Chess，許多基于執(zhí)行的模型檢測(cè)技術(shù)已經(jīng)被結(jié)合在新版本的SPIN中[2,13]；抽象精化模型檢測(cè)器的Yogi工具用于處理指針和程序，它驗(yàn)證有限狀態(tài)機(jī)表示的無效程序的屬性；SLAM主要針對(duì)C語言，不斷的對(duì)抽象的程序模型進(jìn)行細(xì)化和反復(fù)迭代，直至發(fā)現(xiàn)錯(cuò)誤或超時(shí)；BLAST的思想與SLAM類似，BLAST可以集成到Eclipse開發(fā)環(huán)境中，可以提供一個(gè)典型的程序分析問題的斷言檢查；此外，還有其他模型檢測(cè)工具：Java PathFinder、Modechart Toolset、CMC、PRISM、TReX、IOAToolset、MOCHA、PARAGON、SGM、Kronos、Hytech、UPPAAL、VERISOFT、HMC。

3.3 抽象解釋工具

●The C Global Surveyor(CGS)，是一個(gè)針對(duì)航天任務(wù)軟件開發(fā)的靜態(tài)分析器，它用來分析在Mars Path-Finder Finder、Deep SpaceOne和Mars Exploration Rover中使用的軟件。

●PAG，是一個(gè)程序分析器，可以分析與體系結(jié)構(gòu)相關(guān)的特性，如最壞情況下的執(zhí)行時(shí)間、高速緩存的性能、堆棧情況和管道的行為[13]。

●NPCA-WCET[14]，基于抽象解釋的自動(dòng)分析工具，主要面向高級(jí)語言和具有流水線和高速緩存的RISC處理器結(jié)構(gòu)。利用靜態(tài)分析方法得到程序最差情況執(zhí)行時(shí)間的安全估值，再利用其詞法分析和語法分析的功能獲取程序的調(diào)用關(guān)系和語法結(jié)構(gòu)，通過對(duì)源程序的插樁得到程序的結(jié)構(gòu)及分支覆蓋的情況。

●基于抽象解釋分析的其他工具有Proverif和ASTREE，它們可用于大規(guī)模的硬件和軟件系統(tǒng)的驗(yàn)證。

3.4 其他工具

●V-HOLT驗(yàn)證器，自動(dòng)驗(yàn)證的基于高階邏輯的定理證明工具，不需要用戶手工操作[14]；

●codetest，可以對(duì)多種類型功能進(jìn)行分析，包括對(duì)內(nèi)存、性能、代碼覆蓋進(jìn)行分析，也可對(duì)軟件進(jìn)行跟蹤，可對(duì)數(shù)據(jù)的一致性提供保證[15]；

●JUTA，針對(duì)Java語言的自動(dòng)化單元測(cè)試工具，將單個(gè)Java方法的源代碼解析成控制流圖，然后利用符號(hào)執(zhí)行分析路徑，可檢測(cè)程序斷言和特定類型的錯(cuò)誤，并能夠在可接受的時(shí)間內(nèi)給出有效結(jié)果[16]；

●Tamiflex，是一個(gè)工具鏈，可以有效解決靜態(tài)程序分析和java轉(zhuǎn)換的部分問題[17]；

●Splint工具，用于檢測(cè)程序風(fēng)格和注釋，適用于C語言，被成功用于Wu-ftp和Apache的檢測(cè)中；

●PREfix采用符號(hào)執(zhí)行與約束求解的方法對(duì)C/ C++程序進(jìn)行靜態(tài)分析。自動(dòng)PAT采用了布爾邏輯可滿足性算法與線性規(guī)劃結(jié)合的方法，來判斷路徑的可滿足性[9]；

●Checkstyle，是來自SourceForge的開源項(xiàng)目，促使開發(fā)人員遵循規(guī)范編寫代碼，用于檢查程序的編碼格式、約定的命名規(guī)則、類的設(shè)計(jì)等方面。

3.5 靜態(tài)程序分析方法和工具的不足

相比動(dòng)態(tài)分析，靜態(tài)分析考慮執(zhí)行路徑更加全面，漏報(bào)率更低，可以更早的發(fā)現(xiàn)更多的缺陷，適用于狀態(tài)有限、穩(wěn)定性要求較高的軟件。但是動(dòng)態(tài)分析獲取了程序在運(yùn)行過程中的具體信息,所以發(fā)現(xiàn)某些性質(zhì)（程序指針運(yùn)算、動(dòng)態(tài)存儲(chǔ)分配等）缺陷可能更準(zhǔn)確,誤報(bào)率也較低。

靜態(tài)分析的不足：

●靜態(tài)分析方法的誤報(bào)率很高，可能是不可達(dá)路徑判斷不準(zhǔn)確或控制流與數(shù)據(jù)流聚合有問題等造成的；

●靜態(tài)分析精度比動(dòng)態(tài)分析低，受規(guī)模限制較大，分析面窄；

●靜態(tài)分析工具一般比較龐大，對(duì)運(yùn)行環(huán)境要求苛刻；

●靜態(tài)分析工具采用的算法存在片面性，雖然自動(dòng)化程度較高，但某些工具的結(jié)果仍需手工確認(rèn)；

●靜態(tài)分析工具只能檢測(cè)出一部分缺陷，存在漏報(bào)。

4 未解決的問題和未來的工作

由于程序規(guī)模的增大，程序設(shè)計(jì)語言的復(fù)雜性成倍增長，而且證明程序正確與否是一個(gè)比較復(fù)雜的問題，很難達(dá)到高效率且易查錯(cuò)的效果，所以程序驗(yàn)證只應(yīng)用在一部分關(guān)鍵模塊，沒有被廣泛使用。另外在模型構(gòu)造、路徑選擇方面需要開發(fā)更好的策略。

在未來的工作中，研究靜態(tài)和動(dòng)態(tài)結(jié)合的方向有比較高的熱潮，靜態(tài)分析與動(dòng)態(tài)分析的分析精度、開銷和適用的軟件屬性等方面差別很大，所以它們的結(jié)合可以平衡各自的缺點(diǎn)，發(fā)揚(yáng)各自的優(yōu)點(diǎn)。同時(shí)，在限制分析路徑范圍的條件下，將靜態(tài)分析和動(dòng)態(tài)測(cè)試結(jié)合也值得研究，在提高分析結(jié)果精度的同時(shí)，降低了開銷，提高了效率。另外，高精度的程序分析技術(shù)、程序分析新理論和新方法的引入、基于統(tǒng)計(jì)挖掘的軟件分析以及多核技術(shù)對(duì)軟件分析技術(shù)發(fā)展的影響都是未來有潛力的研究方向。

[1]劉磊.程序分析方法[M].北京,機(jī)械工業(yè)出版社,2013.

[2]梅宏,王千祥,張路,王戟.軟件分析技術(shù)進(jìn)展[J].計(jì)算機(jī)學(xué)報(bào).2009(09):1697-710.

[3]Pai M,McCulloch M,Gorman JD,Pai N,Enanoria W,Kennedy G,et al.Systematic Reviews and Meta-Analyses:an Illustrated,Stepby-Step Guide[J].The National medical journal of India.2004,17(2):86.

[4]Mitra RS,Editor Strategies for Mainstream Usage of Formal Verification.Design Automation Conference,2008 DAC 2008 45th ACM/ IEEE;2008 8-13 June 2008.

[5]Jianguo C,HangXia Z,Bruda SD,Editors.Combining Model Checking and Testing for Software Analysis.Computer Science and Software Engineering,2008 International Conference on;2008 12-14 Dec.2008.

[6]楊宇,張健.程序靜態(tài)分析技術(shù)與工具[J].計(jì)算機(jī)科學(xué)，2004(02):171-4.

[7]Jhala R,Majumdar R.Software Model Checking[J].ACM Computing Surveys(CSUR)，2009,41(4):21.

[8]Ganai MK,Chao W,Weihong L,Editors.Efficient State Space Exploration:Interleaving Stateless and State-Based Model Checking. Computer-Aided Design(ICCAD),2010 IEEE/ACM International Conference on;2010 7-11 Nov.2010.

[9]張健.精確的程序靜態(tài)分析[J].計(jì)算機(jī)學(xué)報(bào),2008,09:1549-1553.

[10]Ruthruff JR,Elbaum S,Rothermel G,Editors.Experimental Program Analysis:a New Program Analysis Paradigm.Proceedings of the 2006 International Symposium on Software Testing and Analysis，2006:ACM.

[11]于利前,王林章,雷斌,趙建華,李宣東.靜動(dòng)態(tài)結(jié)合的Java程序不變性分析方法[J].計(jì)算機(jī)學(xué)報(bào).2010(04):736-46.

[12]文昌辭,王昭順.軟件測(cè)試自動(dòng)化靜態(tài)分析研究[J].計(jì)算機(jī)工程與設(shè)計(jì),2005,04:987-989.

[13]D'Silva V,Kroening D,Weissenbacher G.A Survey of Automated Techniques for Formal Software Verification[J].Computer-Aided Design of Integrated Circuits and Systems,IEEE Transactions on，2008,27(7):1165-78.

[14]姬孟洛,李軍,王馨,齊治昌.一種基于抽象解釋的WCET自動(dòng)分析工具[J].計(jì)算機(jī)工程，2006,32(14):54-6.

[15]丁沂.軟件分析技術(shù)與工具[J].無線互聯(lián)科技，2012(04):52.

[16]嚴(yán)俊,郭濤,阮輝,玄躋峰.JUTA:一個(gè)Java自動(dòng)化單元測(cè)試工具[J].計(jì)算機(jī)研究與發(fā)展，2010(10):1840-8.4

[17]Bodden E,Sewe A,Sinschek J,Oueslati H,Mezini M,Editors.Taming Reflection:Aiding Static Analysis in the Presence of Reflection and Custom Class Loaders.Software Engineering(ICSE),2011 33rd International Conference on，2011，21-28 May 2011.

作者簡介：

高婉玲（1992-），女，河南新鄉(xiāng)人，碩士研究生，研究方向?yàn)樾问交?yàn)證、軟件自動(dòng)化測(cè)試

趙鶴（1992-），女，吉林長春人，碩士研究生，學(xué)生，研究方向?yàn)檐浖问交?yàn)證和軟件自動(dòng)化測(cè)試

Static Program Analysis Methods and Tools

GAO Wan-ling，ZHAO He
（College of Computer Science,Sichuan University,Chengdu610065）

Reviews the static program analysis methods and tools.Uses systematic literature review method and bibliometric analysis method,to analyze and summarize the information in a large of papers by collecting,screening and extracting content of papers.Through Endnote,SPSS, and RefViz,the basic information in papers database is added up and analyzed,including age distribution,author distribution,keywords and hotspot analysis.By reading a large number of papers,static program analysis methods can be divided into model checking,symbolic execution,theorem proving,abstract interpretation,etc.Static program analysis tools include formal verification tools,model checking tools and so on.At last,summarizes the shortcomings of static analysis methods and tools.

Program Analysis;Static Analysis Method;Static Analysis Tool;Systematic Literature Review

1007-1423（2017）05-0038-05

10.3969/j.issn.1007-1423.2017.05.010

2016-12-01

2017-01-20