|
|
Lectures
| Aug 30
| Introduction
| pdf
|
|
|
| Sep 5, 10
| Ocaml
| pdf
|
| h1, due Sep. 17
|
| Sep 12, 17
| Induction and Operational Semantics
| pdf
| (Recommended) Chapter 3 of Pierce
| p1, due Oct. 1
|
| Sep 19
| Lambda Calculus
| pdf
| (Recommended) Chapter 5 of
Pierce, available locally as parts 1 and 2.
|
|
| Sep 24, 26, Oct 1
| Type Systems
| pdf (updated 10/1)
| (Recommended) Pierce, Chapter 9, parts 1 and 2, and a typeset version of figure 9-1.
(Recommended) Proofs are Programs: 19th Century Logic and 21st Century Computing
| h2, due Oct. 3
p2, due Oct. 15
|
| Oct 3, 8
| Type Qualifiers
| pdf
| (Optional) Flow-Insensitive
Type Qualifiers, Foster, Johnson, Kodumal, and Aiken
(Optional) Type
Qualifier
Inference for Java, GreenfieldBoyce, Foster
| h3, due Oct. 12 (my
office, by 2pm)
|
| Oct 10, 15
| Data flow analysis
| pdf
(with animations)
| (Recommended) Kildall, A Unified Approach
to Global Program Optimization
(Optional) Chapter 2 from Hankin,
Nielson, and Nielson text (heavy on the notation)
|
h4, due Oct. 22 (in class)
p3, due Oct. 29
|
| Oct 17, 22
| Program Verification (Axiomatic Semantics)
| pdf
|
Recommended: An axiomatic basis for
computer programming, C. A. R. Hoare (only 6 pages!)
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, due Oct. 29 (in class)
|
| Oct 24
| Abstract Interpretation
| pdf (updated 10/25)
|
|
|
| Nov. 5, 7
| Exam
|
|
|
|
| Nov. 12
| FindBugs (guest lecture Bill Pugh)
|
|
|
|
| Oct 29, 31, Nov. 14
| Alias Analysis (applied to data race detection)
| pdf
| (Optional)Context-sensitive Correlation Analysis for Detecting Races, Pratikakis, Foster, and Hicks
|
|
| Nov 19
| 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
|
|
Nov 26, 28
Dec 3
| The Coq proof assistant
|
| propositional logic
overview, Pierce's third lecture
| Coq proofs (optional)
|
| Dec 5
| Project presentations
|
| Aaron Pendergrass
Mike Lam
Bao Nguyen and Ryan Blue
|
|
| Dec 10
| Project presentations
|
| Ben Langmead and Adam Fuchs
Eric Hardisty and Kyle King
Ranjit Kumaresan and Mohammadreza Ghosdi
Sukhyun Song
David An
|
|
| Dec 17
|
|
|
| Project writeups due
|
|