Courses:

Help support MIT OpenCourseWare by shopping at Amazon.com! MIT OpenCourseWare offers direct links to Amazon.com to purchase the books cited in this course. Click on the book titles and purchase the book from Amazon.com, and MIT OpenCourseWare will receive up to 10% of all purchases you make. Your support will enable MIT to continue offering open access to MIT courses.

6.883 is a graduate paper-reading seminar. As such, each class session begins with a brief presentation followed by a discussion of the assigned reading material, which is listed below. To help in preparing for the discussion, each student is asked to write a one-paragraph commentary on the assigned reading the day before the class meets to discuss it.

Jones, Neil D., and Flemming Nielson. "Abstract Interpretation: A Semantics-based Tool for Program Analysis." In Handbook of Logic in Computer Science. New York, NY: Oxford University Press, 1995, pp. 527-629. ISBN: 019853762X. Read first two sections only.

Cousot, Patrick, and Radhia Cousot. "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints." POPL (1977): 238-252.

Ferguson, Roger, and Bogdan Korel. "The Chaining Approach for Software Test Data Generation." ACM TOSEM 5, no. 1 (1996): 63-86.

Ball, Thomas, and James R. Larus. "Efficient Path Profiling." MICRO 29 (1996): 46-57.

Zeller, Andreas, and Ralf Hildebrandt. "Simplifying and Isolating Failure-inducing Input." IEEE TSE 28, no. 2 (2002): 183-200.

Ernst, Michael D., Jake Cockrell, William G. Griswold, and David Notkin. "Dynamically Discovering Likely Program Invariants to Support Program Evolution." IEEE TSE 27, no. 2 (2001): 1-25. Skim sections 5-8; read the rest more carefully.

Damas, Luis, and Robin Milner. "Principal Type-schemes for Functional Programs." In Proc. of the 9th ACM Symp. on POPL. Albuquerque, Mexico, 1982, pp. 207-212. ISBN: 0897910656.

Lee, Oukseh, and Kwangkeun Yi. "Proofs about a Folklore Let-polymorphic Type Inference Algorithm." ACM TOPLAS 20, no. 4 (1998): 707-723.

Reynolds, John C. "Introduction to Part II, Polymorphic Lambda Calculus." In Logical Foundations of Functional Programming. Edited by Gérard Huet. Reading, MA: Addison-Wesley, 1990, pp. 77-86. ISBN: 0201172348.

O'Callahan, Robert, and Daniel Jackson. "Lackwit: A Program Understanding Tool based on Type Inference." ICSE. Boston, MA: 1997, pp. 338-348. ISBN: 0897919149.

Johnson, Robert T., and David Wagner. "Finding User/Kernel Pointer Bugs with Type Inference." In Proc. of USENIX Security Symp. 2004, pp. 119-134.

Steensgaard, Bjarne. "Points-to Analysis in Almost Linear Time." In Proc. of the 23rd ACM Symp. on POPL. St. Petersburg Beach, Florida, 1995, pp. 32-41. ISBN: 0897917693.

———. "Points-to Analysis by Type Inference of Programs with Structures and Unions." In Proc. of 6th Int. Conf. on Compiler Construction. 1996, pp. 136-150. ISBN: 3540610537. Skim for differing material.

Rayside, Derek. "Points-to Analysis." (notes, Massachusetts Institute of Technology, 2005)

Holzmann, Gerard J. "The Spin Model Checker." IEEE TSE 23, no. 5 (1997): 279-295.

Chan, William, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, and William E. Warner. "Optimizing Symbolic Model Checking for Statecharts." IEEE TSE 27, no. 2 (2001): 170-190.

Corbett, James C. "Constructing Compact Models of Concurrent Java Programs." ISSTA 23, no. 2 (1998): 1-10.

Visser, William, SeungJoon Park, and John Penix. "Using Predicate Abstraction to Reduce Object-oriented Programs for Model Checking." In Proc. of the Third Workshop on Formal Methods in Software Practice. Portland, Oregon, 2000, pp. 3-182. ISBN: 158113262X.