|
|
Lectures
Foundations
| 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
| 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
| 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
|
|