6.883: Program Analysis

Fall 2005

Course announcement: HTML, PDF

Thursday, September 8: Assignment 1 (due Tuesday, September 13): PDF, PostScript
Tuesday, September 13: "Abstract Interpretation: a semantics-based tool for program analysis", by Neil Jones and Flemming Nielson. First two sections only. PostScript.
Thursday, September 15: "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints", by Patrick Cousot and Radhia Cousot. POPL 1977. PDF

Tuesday, October 18: "The chaining approach for software test data generation", by Roger Ferguson and Bogdan Korel, TOSEM 1996. PDF
Thursday, October 20: "Efficient path profiling", by Thomas Ball and James R. Larus. MICRO 29. PDF
Tuesday, October 25: "Simplifying and isolating failure-inducing input", by Andreas Zeller and Ralf Hildebrandt. TSE 2002. PDF
Thursday, October 27: "Dynamically discovering likely program invariants to support program evolution" by Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. TSE 2001. Skim sections 5-8; read the rest more carefully. PDF

Tuesday, November 1: "Principal type-schemes for functional programs", by Luis Damas and Robin Milner, POPL 1982. PDF
Tuesday, November 1: "Proofs about a Folklore Let-Polymorphic Type Inference Algorithm", by Oukseh Lee and Kwangkeun Yi. TOPLAS 1998. PDF
Thursday, November 3: "Introduction to Part II, Polymorphic Lambda Calculus", by John C. Reynolds. pages 77-86 in Logical Foundations of Functional Programming, edited by Gérard Huet, Addison-Wesley, 1990. PDF
Tuesday, November 8: "Lackwit: A Program Understanding Tool Based on Type Inference", by Robert O'Callahan and Daniel Jackson. ICSE 1997 PDF
Tuesday, November 8: "Finding User/Kernel Pointer Bugs With Type Inference", by Robert T. Johnson and David Wagner. USENIX Security, 2004. PostScript, PDF
Thursday, November 10: "Points-to Analysis in Almost Linear Time", by Bjarne Steensgaard. In POPL 1996. PostScript, PDF
Thursday, November 10: "Points-to Analysis by Type Inference of Programs with Structures and Unions", by Bjarne Steensgaard. CC 1996. Skim for differing material. PostScript, PDF
Thursday, November 10: Derek Rayside's notes on points-to analysis

Thursday, November 17: "The Spin Model Checker" by Gerard J. Holzmann. IEEE TSE 23(5), 1997. PostScript
Tuesday, November 22: "Optimizing Symbolic Model Checking for Statecharts" by William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, and William E. Warner. IEEE TSE 27(2), 2001. PDF
Tuesday, November 29: "Constructing compact models of concurrent Java programs" by James C. Corbett. ISSTA '98. PDF
Tuesday, November 29: "Using predicate abstraction to reduce object-oriented programs for model checking" by William Visser, SeungJoon Park, and John Penix. Third Workshop on Formal Methods in Software Practice, 2000. PostScript

Tuesday, December 6: "Javarifier: Inferring reference immutability for Java" by Matthew Tschantz, Chen Xiao, and Vineet Sinha
Tuesday, December 6: "Analyzing the static elaboration of hardware descriptions" by Michael Pellauer
Tuesday, December 6: "Automated test-case generation with SAT" by Greg Dennis and Robert Seater
Thursday, December 8: "Annotation-less unit type inference for C" by Philip Guo and Stephen McCamant
Thursday, December 8: "Safe test case reduction" by Brad Howes and David Saff
Tuesday, December 13: "Object control invariants" by Lucy Mendel and Derek Rayside
Tuesday, December 13: "Automatic generation of unit regression tests" by Shay Artzi, Adam Kiezun, Carlos Pacheco, and Jeff Perkins