程序分析原理 Principles of Program Analysis

孫文輝，1999年在中國科學院軟件研究所取得博士學位，北京交通大學計算機學院副教授，研究方向為軟件測試與驗證、網絡管理等，為本科生講授JAVA語言和C++程序設計課程。為研究生講授程序設計語言理論和形式化方法課程，在國內外會議和期刊上發表論文30多篇。

前言
第1章概述1
11什麼是程序分析1
12設置場景2
13數據流分析3
131等式方法3
132基於約束的方法5
14基於約束的分析6
15抽象解釋8
16類型和作用系統11
161註釋類型系統12
162作用系統14
17算法16
18程序轉換17
結束語18
迷你項目18
練習20
第2章數據流分析22
21過程內數據流分析22
211可用表達式分析24
212到達定值分析26
213很忙的表達式分析29
214活躍變量分析31
215派生數據流信息33
22理論性質34
221結構操作語義34
222活躍變量分析的正確性38
23單調框架41
231基本定義43
232案例回顧44
233一個不可分配的例子46
24等式系統的求解47
241MFP解47
242MOP解50
25過程間分析53
251結構操作語義55
252過程內分析與過程間分析56
253顯式使用上下文58
254調用字符串作為上下文61
255假設集作為上下文63
256流敏感與流不敏感64
26形狀分析66
261結構操作語義67
262形狀圖70
263分析的描述73
結束語82
迷你項目84
練習86
第3章基於約束的分析90
31抽象0CFA分析90
311分析的描述91
312分析的明確定義96
32理論性質97
321結構操作語義98
322語義正確性101
323解的存在性104
324餘歸納和歸納的比較106
33語法引導的0CFA分析108
331語法引導的規範108
332解的保持110
34基於約束的0CFA分析111
341解的保持113
342約束的求解113
35添加數據流分析117
351抽象值為冪集117
352抽象值為完全格119
36添加上下文信息122
361均勻kCFA分析123
362笛卡兒積算法127
結束語128
迷你項目130
練習132
第4章抽象解釋135
41一種普通的正確性定義135
411正確性關係136
412表示函數138
413一個較小的擴展139
42不動點的近似141
421加寬算子143
422變窄算子146
43Galois連接149
431Galois連接的性質152
432Galois插入155
44Galois連接的系統的設計方法157
441組件上的組合159
442其他組合方式162
45衍生的操作165
451沿著抽象化函數衍生165
452數據流分析中的應用168
453沿著具體化函數衍生171
結束語174
迷你項目176
練習177
第5章類型和作用系統182
51控制流分析182
511底層類型系統183
512基於類型的分析184
52理論性質187
521自然語義187
522語義正確性189
523解的存在性191
53類型推導算法193
531一個底層類型系統的算法193
532一個控制流分析的算法196
533語法可靠性和完備性200
534解的存在性204
54作用205
541副作用分析206
542異常分析210
543區域推導213
55行為219
551通信分析219
結束語225
迷你項目228
練習231
第6章算法234
61工作列表算法234
611工作列表算法的結構235
612LIFO和FIFO疊代238
62逆後序疊代239
621循環算法242
63在強分量裡疊代243
結束語245
迷你項目247
練習248
附錄A偏序集合250
附錄B歸納和餘歸納258
附錄C圖和正則表達式265
參考文獻272
符號索引283
術語索引287