CMSC 631, Fall 2004

Program Analysis and Understanding

Lectures

Date Subject Slides Reading Assignment
August 31 Introduction pdf None
September 2 Dataflow
analysis
pdf Kildall, A Unified Approach to Global Program Optimization p1
September 7 pdf None h1
September 9 pdf Cytron, Ferrante, Rosen, Wegman, and Zadeck, Efficiently Computing Static Single Assignment Form and the Control Dependence Graph
September 14 Abstract Interpretation pdf Jones and Nielson, Abstract Interpretation: a Semantics-Based Tool for Program Analysis (pp1-30 only)
(Optional) Cousot and Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
h2
September 16 O'Caml txt Optional: Developing applications with Objective Caml
September 21 Lambda Calculus Pierce, Chapter 5 (Handout) h3, p2
September 23 Type Systems Cardelli, Type Systems, sections 1-3
September 28 None h4
September 30 Damas and Milner, Principle Type-Schemes for Functional Programs p3
October 5 None h5
October 7 pdf Foster, Johnson, Kodumal, and Aiken, Flow-Insensitive Type Qualifiers (accessible from umd.edu only)
October 12 pdf Rehof and Fahndrich, Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability h6
October 14 Guest Lecture: Mike Hicks pdf Jim et al, Cyclone: A Safe Dialect of C
October 19 pdf Aiken and Wimmers, Type Inclusion Constraints and Type Inference
October 21 Theorem Proving pdf Hoare, An Axiomatic Basis for Computer Programming p4
Project proposals due
October 26 None
October 28 ppt
examples
Huth and Ryan, chapter 4 (Handout)
November 2 Guest Lecture: Bill Pugh Flanagan and Freund, Type-Based Race Detection for Java Election day!
November 4 Guest Lecture: Mike Hicks ps Smith, Walker, and Morrisett, Alias Types
November 9 Guest Lectures
Tevfik Bultan,
Model Checking
pdf None
November 11 Huth and Ryan, Chapter 3 (Handout)
Lecture notes (see chapter 5 especially)
November 16 Recent Results and Tools Giving a Good Research Talk
ESP: Program Verification of Millions of Lines of Code
November 18 pdf The SLAM Project: Debugging System Software via Static Analysis
November 23 New Directions pdf
November 25 No class -- Thanksgiving
November 30 Project Presenations Gupta and Srivastava, Dynamic Checking of Dangling Pointer References
Jackson, Static Analysis of Perl
Speyer, Partially Automated Refactoring
Strecker, Inferring Developer Activities by Analyzing Successive Versions of Source Code
Weiss and Kobyakov, Design-By-Contract Annotation Set and Runtime Verification for .NET Languages
December 2 Fraser, Automatic Discovery of Integrity Constraints in Binary Kernel Modules
Tran, A Survey on Program Slicing
Clancy and McCann, Dynamically Inferring Static Lockset Annotations in C
Farrell, Subjective Feedback for Introductory Programmers
Sayeed, Abstract Interpretation and Set Constraints in the Type Analysis of Logic Programs
December 7 Arras, Aspect Oriented Programming
Zhao and Ma, Inferring Uniqueness of Factory Methods in Java
Byrd, Integer Overflow Detection Using Integer Range Analysis
Lin, Web Ontology Language Reasoning
Blank, A Survey on Efforts toward Completely Automated Program Verification
December 9 Chen and Nakamura, Using Ownership Types to Check Proxy Design Pattern Use
Lumezanu and Udrea, Rule-Based Model Checking of Network Protocols
Omatick, Application of Theorem Proving to Programs for Numerical Analysis
Halaschek-Wiener and Kolovski, Visualization of CFL-Reachability Graphs

Valid HTML 4.01!