Principles of Program Analysis (Google eBook)

Front Cover
Springer Science & Business Media, Jan 1, 1999 - Computers - 450 pages
4 Reviews
Program analysis concerns static techniques for computing reliable approximate information about the dynamic behaviour of programs. Applications include compilers (for code improvement), software validation (for detecting errors in algorithms or breaches of security) and transformations between data representation (for solving problems such as the Y2K problem). This book is unique in giving an overview of the four major approaches to program analysis: data flow analysis, constraint based analysis, abstract interpretation, and type and effect systems. The presentation demonstrates the extensive similarities between the approaches; this will aid the reader in choosing the right approach and in enhancing it with insights from the other approaches. The book covers basic semantic properties as well as more advanced algorithmic techniques. The book is aimed at M.Sc. and Ph.D. students but will be valuable also for experienced researchers and professionals.
  

What people are saying - Write a review

User Review - Flag as inappropriate

Fucked Fucked up book ,
the authors are probably brain eating cannibalistic fucktards ,
and I am forced to read this fucked up book , coz my supervisor asked me to read this piece of shit , I cant fuckin take this , '
I amma gona burn this mother fucker down , I amma gona burn this mother fucker down ,
I amma gona fuckin kill myself , these motherfuckers dont make any fuckin sense
this book is fucked up beyond all recognition .
DONT EVER READ THIS CRAP
 

Review: Principles of Program Analysis

User Review  - Scott Wisniewski - Goodreads

This book is a HARD read. Really hard. It will blow your mind though. The Knaster-Tarski least fixed point theorem is a beautiful piece of mathematics. Seeing what it can enable in programing languages is life changing. Read full review

Contents

Introduction
1
12 Setting the Scene
3
13 Data Flow Analysis
5
132 The Constraint Based Approach
8
14 Constraint Based Analysis
10
15 Abstract Interpretation
13
16 Type and Effect Systems
17
161 Annotated Type Systems
18
411 Correctness Relations
214
412 Representation Functions
216
413 A Modest Generalisation
219
42 Approximation of Fixed Points
221
421 Widening Operators
224
422 Narrowing Operators
230
43 Galois Connections
233
431 Properties of Galois Connections
239

162 Effect Systems
22
17 Algorithms
25
18 Transformations
27
Concluding Remarks
29
Exercises
31
Data Flow Analysis
35
211 Available Expressions Analysis
39
212 Reaching Definitions Analysis
43
213 Very Busy Expressions Analysis
46
214 Live Variables Analysis
49
215 Derived Data Flow Information
52
22 Theoretical Properties
54
222 Correctness of Live Variables Analysis
60
23 Monotone Frameworks
65
231 Basic Definitions
67
232 The Examples Revisited
70
233 A Nondistributive Example
72
24 Equation Solving
74
242 The MOP Solution
78
25 Interprocedural Analysis
82
251 Structural Operational Semantics
85
252 Intraprocedural versus Interprocedural Analysis
88
253 Making Context Explicit
90
254 Call Strings as Context
95
255 Assumption Sets as Context
99
256 FlowSensitivity versus FlowInsensitivity
101
26 Shape Analysis
104
261 Structural Operational Semantics
105
262 Shape Graphs
109
263 The Analysis
115
Concluding Remarks
128
Mini Projects
132
Exercises
135
Constraint Based Analysis
141
311 The Analysis
143
312 Welldefinedness of the Analysis
150
32 Theoretical Properties
153
322 Semantic Correctness
158
323 Existence of Solutions
162
324 Coinduction versus Induction
165
33 Syntax Directed 0CFA Analysis
168
331 Syntax Directed Specification
169
332 Preservation of Solutions
171
34 Constraint Based 0CFA Analysis
173
341 Preservation of Solutions
175
342 Solving the Constraints
176
35 Adding Data Flow Analysis
182
352 Abstract Values as Complete Lattices
185
36 Adding Context Information
189
361 Uniform kCFA Analysis
191
362 The Cartesian Product Algorithm
196
Concluding Remarks
198
Mini Projects
202
Exercises
205
Abstract Interpretation
211
432 Galois Insertions
242
44 Systematic Design of Galois Connections
246
441 Componentwise Combinations
249
442 Other Combinations
253
45 Induced Operations
258
452 Application to Data Flow Analysis
262
453 Inducing along the Concretisation Function
267
Concluding Remarks
270
Mini Projects
274
Exercises
276
Type and Effect Systems
283
511 The Underlying Type System
284
512 The Analysis
287
52 Theoretical Properties
291
521 Natural Semantics
292
522 Semantic Correctness
294
523 Existence of Solutions
297
53 Inference Algorithms
300
532 An Algorithm for Control Flow Analysis
306
533 Syntactic Soundness and Completeness
312
534 Existence of Solutions
317
54 Effects
319
542 Exception Analysis
325
543 Region Inference
330
55 Behaviours
339
Concluding Remarks
349
Mini Projects
353
Exercises
359
Algorithms
365
611 The Structure of Worklist Algorithms
368
612 Iterating in LIFO and FIFO
372
62 Iterating in Reverse Postorder
374
621 The Round Robin Algorithm
378
63 Iterating Through Strong Components
381
Concluding Remarks
384
Mini Projects
387
Exercises
389
Partially Ordered Sets
393
A2 Construction of Complete Lattices
397
A3 Chains
398
A4 Fixed Points
402
Concluding Remarks
404
Induction and Coinduction
405
B2 Introducing Coinduction
407
B3 Proof by Coinduction
411
Concluding Remarks
415
Graphs and Regular Expressions
417
C2 Reverse Postorder
421
C3 Regular Expressions
426
Concluding Remarks
427
Index of Notation
429
Index
433
Bibliography
439
Copyright

Common terms and phrases

Popular passages

Page 442 - M. Emami, R. Ghiya, and LJ Hendren. Context-sensitive interprocedural points-to analysis in the presence of function pointers.
Page 439 - Ole Agesen, Jens Palsberg, and Michael I. Schwartzbach. Type Inference of SELF: Analysis of Objects with Dynamic and Multiple Inheritance.
Page 452 - AK Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation.
Page 445 - Press, jun 200 1 . [7] S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages. In 22nd ACM Symposium on Principles of Programming Languages, pages 392-401, jan 1995.
Page 451 - J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference.
Page 439 - J. Foster, and Z. Su. A toolkit for constructing type- and constraint-based program analyses. In Proc.
Page 449 - G. Ramalingam, J. Field, and F. Tip. Aggregate structure identification and its application to program analysis. In Symposium on Principles of Programming Languages, pages 119-132, Jan.
Page 440 - Programming, 7(3):321347, 1997. 3. T. Amtoft, F. Nielson, HR Nielson, and J. Ammann. Polymorphic subtyping for effect analysis: The dynamic semantics. In Analysis and Verification of MultipleAgent Languages, volume 1192 of Lecture Notes in Computer Science, pages 172206.
Page 447 - F. Nielson and HR Nielson. From CML to process algebras. In Proc.

Bibliographic information