CMSC 631, Fall 2006

Program Analysis and Understanding

Lectures

Foundations

Date Subject Slides Reading Assignment
Aug 30 Introduction pdf
Sep 6 Dataflow Analysis pdf (Optional) Kildall, A Unified Approach to Global Program Optimization
Chapter 2 from Hankin, Nielson, and Nielson text (heavy on the notation)
p1 (due Sep. 20)
Sep 11 (Stuff in slides on Elimination is "optional") h1 (due Sep. 20)
Sep 13 Operational Semantics pdf (Optional) Chapter 3 of Pierce.
Sep 18
Sep 20 h2 (due Sep. 27)
p2 (due Oct. 4)
Sep 25 OCaml pdf (Optional) Developing Applications in OCaml
Sep 27
Oct 2 Lambda Calculus pdf Recommended: Chapter 5 of Pierce, available locally as parts 1 and 2.
Oct 4 h3
Oct 9 Type Systems pdf Recommended: Pierce, Chapter 9, parts 1 and 2, and a typeset version of figure 9-1.
Optional: Proofs are Programs: 19th Century Logic and 21st Century Computing
Oct 11 p3
h4
Oct 16 Constraint-based Analysis pdf Optional: Type Inclusion Constraints and Type Inference, Aiken and Wimmers
Nov 6 Program Verification (Axiomatic Semantics) pdf Recommended: Huth and Ryan Logic in Computer Science Chapter 4, parts 1, 2, and 3
Optional: Extended Static Checking for Java, Flanagan et al. Download
h5
Nov 8
Nov 13 Abstract Interpretation pdf Optional: Stacktool at Utah h6

Applications

Date Subject Slides Reading Assignment
Oct 18 ESP and Metal ppt Hallem, Chelf, Xie, and Engler, A System and Language for Building System-Specific Static Analyses
Das, Lerner, and Seigle, ESP: Path-Sensitive Program Verification in Polynomial Time
Oct 23 Cyclone pdf Cyclone, a Type-safe Dialect of C, Grossman, Hicks, Jim, and Morrisett
Safe Manual Memory Management in Cyclone, Swamy, Hicks, Morrisett, Grossman, and Jim
Oct 25 Type Qualifiers
(Jeff Foster, guest lecturer)
pdf Flow-Insensitive Type Qualifiers, Foster, Johnson, Kodumal, and Aiken
Oct 30 Types, Effects, and Concurrency Safety Talpin and Jouvelt, Type and Effect Discipline
Flanagan and Abadi, Types for Safe Locking
Nov 1 Locksmith: Finding Race Conditions in C Programs
(Guest Lecturer: Polyvios Pratikakis)
pdf Context-Sensitive Correlation Analysis for Detecting Races
Nov 15 FindBugs: Find Bugs (easily!) in Java programs
(Guest Lecturer: Bill Pugh)
Nov 20 TAL/PCC pdf (slides updated 11/27)
Chapter 4 of Pierce's Advanced Topics in Types and Programming Languages
Nov 27 Technical writing and speaking Giving a good research talk (cached from http://research.microsoft.com/Users/simonpj/papers/giving-a-talk/giving-a-talk.zip)
Writing a good research paper (cached from http://research.microsoft.com/~simonpj/papers/giving-a-talk/writing-a-paper.zip)
Excerpts from Zobel's Writing for Computer Science (UMD access only)

Project Presentations

Date Topic
Nov 29
  • Nat Ayewah: Taking advantage of generics in FindBugs
  • Brian Corcoran: Protecting Cyclone code with a sandboxed native interface
  • Jason Rogers: Improving the quality of network protocols via static analysis
  • Cosmin Craciunescu: A generic front end for C static analysis
Dec 4
  • Machon Gregory: Combining static analysis with SELinux for protecting information flows
  • Rob Patro and Patrick Jenkins: Proving properties about dynamic software updates
  • Kan Leung Cheng and Shanchan Wu: Using CQual to reason about information flows in C programs
Dec 6
  • Charles Song, Chris Hayden, and Chris Ackermann: Discovering opportunites for future-based parallelism in Java programs via dynamic analysis
  • Khoo Yit: User-centered static analysis with CQual
  • Joonghoon Lee and Nick Kuilema: Synchronization inference for Flux programs
Dec 11
  • Elnatan Reisner and Shomir Wilson: Abductive Reasoning for Explaining Errors in Pistacio
  • Sureyya Tarkan: Using Pistacio to check for deadlock in MPI programs
  • Tugrul Ince: A static slicing tool for binaries using DynInst

Valid HTML 4.01!