內容大鋼
本書主要介紹4種程序分析方法——數據流分析、基於約束的分析、抽象解釋、類型和作用系統。涵蓋基本語義屬性和高級演算法。全書共6章，第1章為概述，第2?5章依次為數據流分析、基於約束的分析、抽象解釋、類型和作用系統，第6章為分析演算法介紹。本書基本涵蓋了程序分析領域的經典方法和技術，配以嚴謹的形式化系統，思路清晰、邏輯性強，是學習和研究程序分析原理不可多得的經典書籍。
本書既適合作為程序分析相關碩博研究生課程的教材，也適合相關專業研究人員和專業人士閱讀。
作者介紹
(丹)弗萊明·尼爾森//漢內·里斯·尼爾森//(英)克里斯·漢金|責編:張秀華|譯者:詹博華//冀振燕//孫文輝
目錄
第1章 概述
1.1 什麼是程序分析
1.2 設置場景
1.3 數據流分析
1.3.1 等式方法
1.3.2 基於約束的方法
1.4 基於約束的分析
1.5 抽象解釋
1.6 類型和作用系統
1.6.1 註釋類型系統
1.6.2 作用系統
1.7 演算法
1.8 程序轉換
結束語
迷你項目
練習
第2章 數據流分析
2.1 過程內數據流分析
2.1.1 可用表達式分析
2.1.2 到達定值分析
2.1.3 很忙的表達式分析
2.1.4 活躍變數分析
2.1.5 派生數據流信息
2.2 理論性質
2.2.1 結構作語義
2.2.2 活躍變數分析的正確性
2.3 單調框架
2.3.1 基本定義
2.3.2 案例回顧
2.3.3 一個不可分配的例子
2.4 等式系統的求解
2.4.1 MFP解
2.4.2 MOP解
2.5 過程間分析
2.5.1 結構作語義
2.5.2 過程內分析與過程間分析
2.5.3 顯式使用上下文
2.5.4 調用字元串作為上下文
2.5.5 假設集作為上下文
2.5.6 流敏感與流不敏感
2.6 形狀分析
2.6.1 結構作語義
2.6.2 形狀圖
2.6.3 分析的描述
結束語
迷你項目
練習
第3章 基於約束的分析
3.1 抽象0-CFA分析
3.1.1 分析的描述
3.1.2 分析的明確定義
3.2 理論性質
3.2.1 結構作語義
3.2.2 語義正確性
3.2.3 解的存在性
3.2.4 余歸納和歸納的比較
3.3 語法引導的0-CFA分析
3.3.1 語法引導的規範
3.3.2 解的保持
3.4 基於約束的0-CFA分析
3.4.1 解的保持
3.4.2 約束的求解
3.5 添加數據流分析
3.5.1 抽象值為冪集
3.5.2 抽象值為完全格
3.6 添加上下文信息
3.6.1 均勻k-CFA分析
3.6.2 笛卡兒積演算法
結束語
迷你項目
練習
第4章 抽象解釋
4.1 一種普通的正確性定義
4.1.1 正確性關係
4.1.2 表示函數
4.1.3 一個較小的擴展
4.2 不動點的近似
4.2.1 加寬運算元
4.2.2 變窄運算元
4.3 Galois連接
4.3.1 Galois連接的性質
4.3.2 Galois插入
4.4 Galois連接的系統的設計方法
4.4.1 組件上的組合
4.4.2 其他組合方式
4.5 衍生的作
4.5.1 沿著抽象化函數衍生
4.5.2 數據流分析中的應用
4.5.3 沿著具體化函數衍生
結束語
迷你項目
練習
第5章 類型和作用系統
5.1 控制流分析
5.1.1 底層類型系統
5.1.2 基於類型的分析
5.2 理論性質
5.2.1 自然語義
5.2.2 語義正確性
5.2.3 解的存在性
5.3 類型推導演算法
5.3.1 一個底層類型系統的演算法
5.3.2 一個控制流分析的演算法
5.3.3 語法可靠性和完備性
5.3.4 解的存在性
5.4 作用
5.4.1 副作用分析
5.4.2 異常分析
5.4.3 區域推導
5.5 行為
5.5.1 通信分析
結束語
迷你項目
練習
第6章 演算法
6.1 工作列表演算法
6.1.1 工作列表演算法的結構
6.1.2 LIFO和FIFO迭代
6.2 逆後序迭代
6.2.1 循環演算法
6.3 在強分量里�
[