CSE 503: Software Engineering: Program Analysis

Winter 2010

Meetings: MW 10:30-11:50, room MGH 238

TA: Todd Schiller

Mailing list: CSE503@cs
(To send mail to the list, you must send use your @u address, not a @cs, @google.com, etc. address. Let us know if this is a hardship, and we will add your other address to the list of permitted senders.)

Introduction: Static and dynamic analysis

Monday, January 4: Lecture 1: Overview of topics, Static and dynamic analysis

Abstract interpretation

Monday, January 4: Assignment 1 (due Wednesday, January 6)
Wednesday, January 6: "Abstract Interpretation: a semantics-based tool for program analysis", by Neil Jones and Flemming Nielson. First two sections only. PostScript.
Monday, January 11: "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

Dynamic analysis

Wednesday, February 3: "Simplifying and isolating failure-inducing input", by Andreas Zeller and Ralf Hildebrandt. TSE 2002. PDF
Wednesday, February 3: "DART: Directed automated random testing", by Patrice Godefroid, Nils Klarlund, and Koushik Sen. PLDI 2005. PDF
Monday, February 8: "Efficient path profiling", by Thomas Ball and James R. Larus. MICRO 29. PDF
Monday, February 8: "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

Model checking

Wednesday, February 10: "The Model Checker SPIN" by Gerard J. Holzmann. IEEE TSE 23(5), 1997. PDF
Wednesday, February 17: "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
Presenters: Prasang Upadhyaya, Yingyi Bu
Wednesday, February 17: "Counterexample-Guided Abstraction Refinement", by Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. CAV 2000. PDF
Presenters: Sai Zhang, Chris Hacking
Monday, February 22: "CMC: a pragmatic approach to model checking real code" by Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, and David L. Dill. In OSDI 2002. PostScript
Presenters: Aditya Sankar, Sigurd Schneider
Monday, February 22: "Finding and Reproducing Heisenbugs in Concurrent Programs" by Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. OSDI 2008. PDF
Presenters: Ivan Beschastnikh, Janara Christensen

Types

Wednesday, February 24: Wikipedia on lambda calculus
"Principal type-schemes for functional programs", by Luis Damas and Robin Milner, POPL 1982. PDF. There is a typo in Algorithm W part (ii): on the second line, e2 and t2 should be e1 and t1. "e2" and "t2" are correct on third line.
Chapter 30 (book pages 273-283, which are pages 289-299 in the PDF) of Programming Languages: Application and Interpretation by Shriram Krishnamurthi.
Monday, March 1: "Lackwit: A Program Understanding Tool Based on Type Inference", by Robert O'Callahan and Daniel Jackson. ICSE 1997. PDF
Presenter: Gilbert Bernstein [Lecture Notes]
Monday, March 1: "Dynamic inference of abstract types", by Philip J. Guo, Jeff H. Perkins, Stephen McCamant, and Michael D. Ernst. ISSTA 2006. Essentially the Lackwit paper, implemented dynamically rather than statically. PDF
Presenter: Joshua Goodwin [Lecture Slides]
Monday, March 1: "Finding User/Kernel Pointer Bugs With Type Inference", by Robert T. Johnson and David Wagner. USENIX Security, 2004. PostScript, PDF
Presenters: Michael Bayne, Reto Conconi [Lecture Slides]

Pointer analysis

Wednesday, March 3: "Pointer Analysis: Haven't We Solved This Problem Yet?" In PASTE 2001. PostScript
Wednesday, March 3: Derek Rayside's notes on points-to analysis
Monday, March 8: "Points-to Analysis in Almost Linear Time", by Bjarne Steensgaard. In POPL 1996. PostScript, PDF
Presenters: Erik Andersen, Michael Ratanapintha [Lecture Slides]
Monday, March 8: "Points-to Analysis by Type Inference of Programs with Structures and Unions", by Bjarne Steensgaard. CC 1996. Significant overlap with POPL 96 paper. Skim for differing material. PostScript, PDF
Presenters: Slava Chernyak, Colin Gordon [Lecture Slides]
Monday, March 8: "Strictly Declarative Specification of Sophisticated Points-to Analyses", by Martin Bravenboer and Yannis Smaragdakis. OOPSLA 2009. PDF
Presenters: Shiri Azenkot, Evan Herbst [Lecture Slides]

Verification

Wednesday, March 10: "Verification of object-oriented programs with invariants" by Mike Barnett, Robert DeLine, Manuel Fahndrich, K. Rustan M. Leino, and Wolfram Schulte. JOT, 2004. PDF
Presenters: Saleema Amershi, Xiao Sophia Wang [Lecture Slides]