該書共分為6章，其中第1章為介紹，第2~5章依次為數據流分析、基于約束的分析、抽象解釋、類型和作用系統(tǒng)，第6章為分析算法介紹。該書內容基本囊括了程序分析領域中的經典方法和技術，配以嚴謹的形式化系統(tǒng)，全書思路清晰、邏輯性強，是不可多得的經典書籍。
前言
第1章概述1
11什么是程序分析1
12設置場景2
13數據流分析3
131等式方法3
132基于約束的方法5
14基于約束的分析6
15抽象解釋8
16類型和作用系統(tǒng)11
161注釋類型系統(tǒng)12
162作用系統(tǒng)14
17算法16
18程序轉換17
結束語18
迷你項目18
練習20
第2章數據流分析22
21過程內數據流分析22
211可用表達式分析24
212到達定值分析26
213很忙的表達式分析29
214活躍變量分析31
215派生數據流信息33
22理論性質34
221結構操作語義34
222活躍變量分析的正確性38
23單調框架41
231基本定義43
232案例回顧44
233一個不可分配的例子46
24等式系統(tǒng)的求解47
241MFP解47
242MOP解50
25過程間分析53
251結構操作語義55
252過程內分析與過程間分析56
253顯式使用上下文58
254調用字符串作為上下文61
255假設集作為上下文63
256流敏感與流不敏感64
26形狀分析66
261結構操作語義67
262形狀圖70
263分析的描述73
結束語82
迷你項目84
練習86
第3章基于約束的分析90
31抽象0CFA分析90
311分析的描述91
312分析的明確定義96
32理論性質97
321結構操作語義98
322語義正確性101
323解的存在性104
324余歸納和歸納的比較106
33語法引導的0CFA分析108
331語法引導的規(guī)范108
332解的保持110
34基于約束的0CFA分析111
341解的保持113
342約束的求解113
35添加數據流分析117
351抽象值為冪集117
352抽象值為完全格119
36添加上下文信息122
361均勻kCFA分析123
362笛卡兒積算法127
結束語128
迷你項目130
練習132
第4章抽象解釋135
41一種普通的正確性定義135
411正確性關系136
412表示函數138
413一個較小的擴展139
42不動點的近似141
421加寬算子143
422變窄算子146
43Galois連接149
431Galois連接的性質152
432Galois插入155
44Galois連接的系統(tǒng)的設計方法157
441組件上的組合159
442其他組合方式162
45衍生的操作165
451沿著抽象化函數衍生165
452數據流分析中的應用168
453沿著具體化函數衍生171
結束語174
迷你項目176
練習177
第5章類型和作用系統(tǒng)182
51控制流分析182
511底層類型系統(tǒng)183
512基于類型的分析184
52理論性質187
521自然語義187
522語義正確性189
523解的存在性191
53類型推導算法193
531一個底層類型系統(tǒng)的算法193
532一個控制流分析的算法196
533語法可靠性和完備性200
534解的存在性204
54作用205
541副作用分析206
542異常分析210
543區(qū)域推導213
55行為219
551通信分析219
結束語225
迷你項目228
練習231
第6章算法234
61工作列表算法234
611工作列表算法的結構235
612LIFO和FIFO迭代238
62逆后序迭代239
621循環(huán)算法242
63在強分量里迭代243
結束語245
迷你項目247
練習248
附錄A偏序集合250
附錄B歸納和余歸納258
附錄C圖和正則表達式265
參考文獻272
符號索引283
術語索引287
書單推薦
