|
|
Lecture Material and Assignments
Lecture Material
- Lecture 1 - Introduction
- Lectures 2,3 - OCaml
- Lecture 4 - Symbolic execution
and Directed symbolic execution
- Lectures 5,6 - Data flow analysis
- Lecture 7 - Static Single Assignment form
- Lecture 8 - Software Foundations, Basics.v
- See the resources page for
links to the Coq distribution, and Proof General
- Lectures 9, 10 - Lists.v,
Poly.v,
InClass1.v
- Lecture 11 - Gen.v,
Prop.v, Logic.v,
InClass2.v
- Lecture 12 - ESP and ESPX
- Lecture 13, 14 - Imp.v (requires Sflib.v)
- Lecture 15 - InClass3.v, Rel.v, Smallstep.v,
- Lecture 16 - Lambda Calculus
- Lecture 17, 18 - Type
systems
- Lecture 19 - Type inference
- Lecture 20 - Stlc.v
- Lectures 21, 22 - Type
qualifiers (including inference and application to security problems)
- Lecture 23 - Abstract interpretation (slides due to David Schmidt)
- Lectures 24, 25 - Dynamic
enforcement of knowledge-based security policies (updated 11/30/11)
- Lecture 26 - (Optional) Language-based information flow security,
How to write a research paper and How
to give a research talk.
- Project presentations
- Dec. 5 - Karla Saur, Kris Micinski, Adil Yalcin and Philip Yang
- Dec. 7 - Holman Gao, Konstantinos Zampogiannis, James Parker
- Dec. 12 - Qianwen Li, Jane Ren and Anupam Guha, Marshall Swindell
Projects
|