## Principles of Program AnalysisProgram 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

Not an easy read. Definitely not for beginners .

### 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 |

433 | |

439 | |

### Other editions - View all

Principles of Program Analysis Flemming Nielson,Hanne R. Nielson,Chris Hankin No preview available - 2010 |

### Common terms and phrases

0-CFA analysis Abstract Interpretation abstract location algorithm algorithm of Table annotated types annotation variables Ascending Chain Condition assignment axioms Chapter clause coinduction complete lattice computation consider constraint system construct context Control Flow Analysis Data Flow Analysis define edges element evaluate Example Exercise expression final(S flow graph flow(S follows formulation function abstraction Galois connection Galois insertion greatest fixed point HCFA heap hence induction inference iteration labels language least fixed point least solution Lemma lfp(f loop LVerit Mini Project Monotone Framework monotone function node obtained Operational Semantics partially ordered set path program analysis program point proof properties RDentry RDerit Reaching Definitions recursive result reverse postorder rule Section semantic correctness sequence shape graphs specified step strong components Subsection subtyping syntax directed transfer functions Type and Effect type system type variables upper bound widening operator worklist algorithm

### 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.