CS 528/428 Schedule, Spring 2009

1/12:

Lecture: Overview

1/14:

Lecture: Certified Software; Hoare Logic

1/16:

Lecture: Separation Logic

---

1/19:

NO CLASS (MLK day)

1/21:

NO CLASS (POPL'09)

---

1/26:

Lecture: More on Separation Logic; The Coq Proof Assistant

1/28:

Lecture: Certified Assembly Programming (CAP)

---

2/2:

Lecture: Rely-Guarantee Reasoning (CCAP); Concurrent Separation Logic (CSL)

2/4:

Lecture: More on CSL; Permission Accounting

---

2/9:

Lecture: CSL meets Rely-Guarantee (LRG, SAGL, RGSep)

2/11:

Lecture: More on RGSep/LRG; Certified Thread Implementation

---

2/16:

Lecture: Meta-Logic Framework; Proof Engineering

2/18:

Lecture: Singularity; Spec# and Sing#

---

2/23:

Lecture: Decentralized Information Flow Control

2/25:

Lecture: HiStar/DStar/Loki and Flume

---

3/2:

Lecture: Security-Typed Languages (JIF)

3/4:

Lecture: Noninterference; Declassification

---

3/9:

NO CLASS (spring recess)

3/11:

NO CLASS (spring recess)

---

3/16:

NO CLASS (spring recess)

3/18:

NO CLASS (spring recess)

---

3/23:

Lecture: DOM and Context Logic

3/25:

Lecture: (class meets in 307 AKW instead!) JavaScript and Mashup Security

---

3/30:

Lecture: Assertion Lang vs Specification Lang

4/1:

Lecture: Automated Program Verifier (Boogie & Z3)

---

4/6:

Lecture: The SPARK Approach

4/8:

Lecture: Liveness Property

---

4/13:

Lecture: Certified Compiler (CompCert)

4/15:

Lecture: Translation Validation

---

4/20:

Lecture: Secure Voting Systems

4/22:

Lecture: GWT, Json and Caja

---

4/29:

Project presentation (tentative)