CS 528/428 Schedule and Lecture Notes, Spring 2024

1/16:

Lecture: Overview (L01.pdf)

1/18:

Lecture: Logical Foundations and Coq (L02.pdf; Preface; Basics; Induction; Lists)

---

1/23:

Lecture: Hints and Principles for Computer System Design (L03b.html and L03a.html)

1/25:

Lecture: More on Logical Foundations & Coq (Induction; Lists; Poly; Tactics)

---

1/30:

Lecture: Spec, Implementation, Abstraction Function, and Invariant (Lampson Lecture Notes)

2/1:

Lecture: C Memory Model and Clight (related papers and CompCert implementation: Integers, Values, Memdata, and Memory)

---

2/6:

Lecture: Compiler Verification (tutorial and Imp and Compil)

2/8:

Lecture: Clight and Asm in CompCert; Forward & Backward Simulation (L08.pdf; CompCert implementation: Clight, Asm, Smallstep, and Globalenvs)

---

2/13:

Lecture: Certified Abstraction Layers and mCertiKOS (L09.pptx and mCertiKOS and L09b.pdf and POPL15 and POPL22 papers)

2/15:

Lecture: Layered and Object-Based Game Semantics (L09b.pdf and POPL22 paper)

---

2/20:

Lecture: Certified Concurrent Abstraction Layers and mC2 (L10.pptx and L11.pdf and mC2)

2/22:

Lecture: Linearizability and Compositional CCAL (L12.pdf and POPL23 paper)

---

2/27:

Lecture: Information-Flow Security for mCertiKOS (reading and L13.pdf)

2/29:

Lecture: Robust Declassification and A Lattice of Information (CSFW01 and CSFW93 and L14.pdf)

---

3/5:

Lecture: Asynchronous Event-Driven Programming (P and ModP papers and the P Framework website and L15.pdf)

3/7:

Lecture: Statecharts (paper.pdf and L16.pdf); The Compositional Architecture of the Internet (paper.pdf and slides.pdf)

---

3/26:

Lecture: Linear Logic (comp-interp.pdf, tutorial.pdf, BLL, Graded Modal Types / Coeffects, and L17.pdf)

3/28:

Lecture: Robust Property Preservation for Secure Compilation (CSF19 and TOPLAS21 and UC-is-RC paper)

---

4/2:

Lecture: LLM-Aided Verifiable Code Generation (Clover, Alchemist)

4/4:

Lecture: Rust Semantics and C-to-Rust Translation (RustBelt, StackedBorrows, C2Rust, and Ownership-Guided C2Rust)

---

4/9:

Lecture: Equality Saturation and Rewrite Inference (egg and Ruler)

4/11:

Lecture: Graph Library Verification (CoqWigderson, SW-PhD, SW-OOPSLA19 and GraphsCoq)

---

4/16:

Lecture: LLMs for Automated Reasoning (Baldur, Expert-Iteration, Thor, Draft-Sketch-Prove, HyperTree, GPT-f, and pptx slides)

4/18:

Lecture: Zero Knowledge Proofs (Coda, Leo, and ZKCircuits)

---

4/23:

Lecture: ZKSMT (CCS24) and LiDO (PLDI24)

4/25:

Lecture: Linearizability and Relaxed Consistency (IFM18 and POPL19)