|
|
Lectures
| Jan 26
| Introduction
| pdf
|
|
|
| Jan 31
| Data Flow
| pdf
| (Optional) Kildall, A Unified Approach
to Global Program Optimization
| p1
|
| Feb 2
|
| h1
|
| Feb 7
| 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
|
|
| Feb 9
| pdf
| Cytron, Ferrante, Rosen, Wegman, and Zadeck,
Efficiently
Computing Static Single Assignment Form and the Control Dependence Graph
|
|
| Feb 14
| Abstract Interpretation
| pdf
|
(Optional) Cousot and Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
| h2
|
| Feb 16
| OCaml
| pdf
|
| p2
|
| Feb 21
|
|
|
| Feb 23
| Lambda Calculus
| pdf
| Pierce, chapter 5 (handout)
| h3
|
| Feb 28
| Type Systems
| pdf
| Pierce, chapter 9 (handout)
| p3
|
| Mar 2
|
| h4
|
| Mar 7
|
|
|
| Mar 9
| Type Qualifiers
| pdf
|
| h5
|
| Mar 14
|
|
|
| Mar 16
|
|
|
| Mar 21
| No class -- Spring break
|
| Mar 23
|
| Mar 28
| Guest lecture:
Bill Pugh
| pdf
|
|
|
| Mar 30
| Guest lecture:
Mike Hicks
| pdf
|
|
|
| Apr 4
| Axiomatic
Semantics
| pdf
|
|
|
| Apr 6
| pdf
examples
|
| p4
|
| Apr 11
|
|
|
| Apr 13
| Model
Checking
| pdf
|
|
|
| Apr 18
|
|
|
| Apr 20
| ppt
|
|
|
| Apr 25
| Research
| ppt,
ppt
|
|
|
| Apr 27
| FFIs
| pdf
|
|
|
| May 2
| New Directions
| pdf
|
|
|
| May 4
| Project
Presentations
|
|
Gerardo Simari and and Amy Sliva
Sorelle Friedler and Carlos Castillo
Alex Tzannes
|
|
| May 9
|
|
Bhargav Shamanna
Denis Filimonov
Nilay Pahd
|
|
| May 11
|
|
Nir Peer
|
|
|