靜態程序分析

有些程序分析需要在程序運行時才能進行，這種程序分析稱為動態程序分析。部份的靜態程序分析的對象是針對特定版本的源代碼，也有些靜態程序分析的對象是目標代碼。靜態程序分析一詞多半是指配合靜態程序分析工具進行的分析，人工進行的分析一般稱為程序理解（英語：programcomprehension）或代碼審查。

靜態程序分析的複雜程度依所使用的工具而異，簡單的只考慮個別敍述及聲明的行為，複雜的可以分析程序的完整源代碼。不同靜態程序分析產生的信息也有所不同，簡單的可以是標示可能的代碼錯誤（如lint編程工具（英語：lintprogrammingtool）），複雜的可以是形式化方法，也就是用數學的方式證明程序的某些行為符合其設計規格。

軟件度量和反向工程可以視為一種靜態程序分析的方式。在實務上，在定義所謂的軟件品質指針（softwarequalityobjectives）後，軟件度量的推導及程序分析常一起進行，在開發嵌入式系統時常會用這種方式進行。 ^[1] 

靜態程序分析的商業用途可以用來驗證安全關鍵計算機系統中的軟件，並指出可能有計算機安全隱患的代碼，這類的應用越來越多。例如以下的產業已確定用靜態程序分析作為提升複雜軟件品質的方法：

醫療軟件：美國的美國食品藥品監督管理局確定在醫療設備上使用靜態程序分析。

核能軟件：英國的健康與安全委員會（英語：HealthandSafetyExecutive）建議針對堆保護系統（英語：ReactorProtectiveSystem）的軟件進行靜態程序分析中。

在信息安全的領域中，靜態程序分析會稱為靜態應用程序安全檢測（StaticApplicationSecurityTesting，簡稱SAST）。 ^[2] 

形式化方法是一種利用純粹數學的方式分析軟件的方法，應用到的數學技巧包括指稱語義、公理語義、操作語義學及抽象釋義等計算機科學中的方法。

針對任何圖靈完全的編程語言，不可能存在一算法可以找出任意程序在運行期間的所有錯誤，也沒有數學方法可以得到一程序是否會有運行期間的錯誤的結果。上述的結論是由庫爾特·哥德爾、阿隆佐·邱奇及阿蘭·圖靈在1930年代研究停機問題所得的結果。不過如同許多不可判定問題一様，在實務仍會設法找到有用的近似解。

以下是一些形式化靜態分析的實現方式：