Reading List for CSE291 Winter 05

Type systems/Constraints

Foundations

[DM82] Luis Damas and Robin Milner: Principal type-schemes for functional programs. ACM POPL 1982: 207-212.

[Ca97] Luca Cardelli: Type Systems. In the Computer Science and Engineering Handbook 1997:2208-2236.

[Ai99] Alexander Aiken: Introduction to Set Constraint-Based Program Analysis. Science of Computer Programming 35(2): 79-111 (1999).

Applications

[OJ97] Robert O'Callahan, Daniel Jackson: Lackwit: A Program Understanding Tool Based on Type Inference. ICSE 1997: 338-348.

[STFW01] Umesh Shankar, Kunal Talwar, Jeff Foster and David Wagner. Detecting Format-String Vulnerabilities with Type Qualifiers. USENIX Security, 2001.

[STFW01] Robert T. Johnson Shankar and David Wagner. Finding User/Kernel Pointer Bugs With Type Inference. USENIX Security, 2004.

[FF00] Cormac Flanagan, Stephen N. Freund: Type-based race detection for Java. PLDI 2000: 219-232.

[FQ03] Cormac Flanagan and Shaz Qadeer. A Type and Effect System for Atomicity. PLDI 2003.

[WFBA00] David Wagner, Jeff Foster, Eric Brewer, and Alex Aiken. A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. NDSS 2000.

[GCMRJ03] V. Ganapathy et. al. Buffer Overrun Detection using Linear Programming and Static Analysis. ACM Conference on Computer and Communications Security (CCS) 2003.


Dataflow Analysis/Abstract Interpretation

Foundations

[K73] Gary A. Kildall. A Unified Approach to Global Program Optimization. POPL 1973 : 194-206.

[CC77] Patrick Cousot and Radhia Cousot: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977: 238-252.

[NNH] Flemming Nielson, Hanne Riis Nielson and Chris Hankin: Principles of Program Analysis.

[RHS95] Thomas Reps, Susan Horwitz and Mooly Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995.

[BR01a] Thomas Ball and Sriram Rajamani. Bebop: A Path-sensitive Interprocedural Dataflow Engine.

Applications

[E96] David Evans. Static Detection of Dynamic Memory Errors PLDI 1996.

[DLS02] Manuvir Das, Sorin Lerner and Mark Seigle. ESP: Path-Sensitive Program Verification in Polynomial Time. PLDI 2002.

[HCXE02] Seth Hallem, Benjamin Chelf, Yichen Xie, Dawson R. Engler: A System and Language for Building System-Specific, Static Analyses. PLDI 2002: 69-82.

[EA03] Dawson Engler and Ken Ashcraft: RacerX: effective, static detection of race conditions and deadlocks. SOSP 2003: 237-252.

[CJ03] M. Christodorescu and S. Jha: Static Analysis of Executables to Detect Malicious Patterns. Usenix Security Symposium, August 2003.

[BCC+02] Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jirtme Feret, Laurent Mauborgne, Antoine Mini, David Monniaux, Xavier Rival: A Static Analyzer for Large Safety-Critical Software. PLDI 2003.

[GSD04] Carl Gould, Zhendong Su, and Premkumar Devanbu: Static Checking of Dynamically Generated Queries in Database Applications.ICSE 2005.


Deductive Methods.

Foundations

[F67] Robert W. Floyd: Assigning meanings to programs. Amer. Math. Soc. Symposia in Applied Mathematics, volume 19, pages 19--31, 1967.

[H69] C. A. R. Hoare: An Axiomatic Basis for Computer Programming. CACM 12(10): 576-580 (1969).

[H71] C. A. R. Hoare: Proof of a program: FIND. CACM 14(1): 39-45 (1971).

[N80] Greg Nelson: Techniques for Program Verification.Ph.D. Thesis. 1980.

Applications

[NL96] George Necula and Peter Lee: Safe Kernel Extensions Without Run-Time Checking. Safe Kernel Extensions Without Run-Time Checking. OSDI 1996.

[BPS00] William R. Bush, Jonathan D. Pincus, David J. Sielaff: A static analyzer for finding dynamic programming errors. Software - Practice and Experience 30(7): 775-802 (2000).

[FLL+02] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata: Extended Static Checking for Java. PLDI 2002: 234-245.

[DRS03] Nurit Dor, Michael Rodeh and Mooly Sagiv: CSSV: towards a realistic tool for statically detecting all buffer overflows in C PLDI 2003: 155-167.


Model Checking

Foundations

[CGP00] Edmund M. Clarke, Orna Grumberg and Doron A. Peled: Model Checking. MIT Press, 2000.

[BCM+90] J. Burch, E. M. Clarke, K. L. McMillan, D. Dill, J. Hwang : Symbolic Model Checking: 10^20 States and Beyond. LICS, 1990.

[B86] Randal Bryant : Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, Vol. C - 35, No. 8, August, 1986, pp. 677 - 691.

[G97] Patrice Godefroid: Model Checking for Programming Languages using VeriSoft. POPL 1997.

[GS97] Susanne Graf and Hassen Saidi: Construction of Abstract State Graphs with PVS. CAV 1997: 72-83.

Applications

[CW02] Hao Chen and David Wagner: MOPS: an infrastructure for examining security properties of software. CCS 02

[G02] Patrice Godefroid: Software Model Checking in Practice: An Industrial Case Study. ICSE 2002.

[YTEM04] Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal Musuvathi: Using Model Checking to Find Serious File System Errors.OSDI 2004.

[BR01b] Thomas Ball and Sriram Rajamani: Automatically Validating Temporal Safety Properties of Interfaces. SPIN 2001, Workshop on Model Checking of Software, LNCS 2057, May 2001, 103-122.

[HJMS02] Thomas Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre: Lazy Abstraction. POPL 2002.