CS 528/428 Schedule and Lecture Notes, Fall 2014

CS 528/428 Schedule and Lecture Notes, Fall 2014

Last modified: September 9, 2014. This page is still under construction!


8/28:
Lecture: Overview (L1.pdf)

9/2:
Lecture: Hints on Programming Language Design (L2.html)
9/4:
Lecture: SF (Overview; Basics; Induction; Lists; Poly)

9/9:
Lecture: Hints and Principles for Computer System Design (L4.html)
9/11:
Lecture: SF (MoreCoq; Logic)

9/16:
Lecture: Virtual Machine Monitors (L6.html)
9/18:
Lecture: SF (Prop; MoreLogic)

9/23:
Lecture: Microkernels and seL4 (L8.html)
9/25:
Lecture: SF (Imp)

9/30:
Lecture: Capability-Based Systems
10/2:
Lecture: SF (Equiv)

10/7:
Lecture: seL4 (Part 1)
10/9:
Lecture: SF (Hoare; Hoare2)

10/14:
Lecture: seL4 (Part 2)
10/16:
Lecture: SF (SmallStep; Auto)

10/21:
Lecture: HiStar (vs. Flume and Asbestos)
10/23:
NO CLASS (fall recess)

10/28:
Lecture: CertiKOS Overview
10/30:
Lecture: Clight and CompCert

11/4:
Lecture: ClightX Evaluation Semantics
11/6:
Lecture: Verifying ClightX Programs

11/11:
Lecture: mCertiKOS Implementation
11/13:
Lecture: Compiler Verification

11/18:
Lecture: Specs and Code
11/20:
Lecture: Abstraction Functions and Invariants

12/2:
Lecture: File Systems
12/4:
Lecture: TBA

Copyright (c) 2009-2014, Zhong Shao, Dept. of Computer Science, Yale University