抽象解釋(Abstract Interpretation)是形式化驗證方法(Formal Verification)的一種,其餘的兩種分別為定理證明(Theorem Proving)和模型檢驗(Model Checking)。主要是利用形式化的方法對計算機硬體與軟體進行分析驗證。
基本介紹
- 中文名：抽象解釋
- 外文名：Abstract Interpretation
抽象解釋理論產生於Cousot.P和Cousot.R於1977年提出的程式靜態分析時構造和逼近(approxiamation)程式不動點語義的理論。他們討論了基於抽象解釋理論的程式變換，程式安全性(safety)驗證和活性(liveness)的驗證。他們利用抽象解釋理論作為一種新的形式化驗證方法的框架，將各種不同驗證工具的近似理論進行統一。
由於模型檢驗的方法受到狀態空間爆炸的限制，定理證明也由於一階邏輯半可判定的問題，形式化的驗證技術難以廣泛使用。抽象解釋在處理複雜的計算問題或模型的過程中通過對問題進行近似抽象，取出其中的關鍵部分進行分析，從而減少問題的複雜程度，再綜合其他的形式化方法來解決問題。
