Schedule. The following schedule is only an approximate and is subject to change.

  Date Topics Slides and readings Homework
Week 1 8/23, 8/25 Introduction; functional programming in Coq Introduction; SF book: Preface and Basics chapters HW1 due on Aug 31st
Week 2 8/30, 9/1 Proof by induction; lists SF book: Induction and Lists chapters HW2 due on Sep 7th
Week 3 9/6, 9/8 Polymorphism SF book: Poly chapter HW3 due on Sep 14th
Week 4 9/13, 9/15 Tactics for automation SF book: Tactics chapter HW4 due on Sep 21st
Week 5 9/20, 9/22 Logic in Coq; Inductively defined propositions SF book: Logic and IndProp chapters HW5 due on Sep 28th
Week 6 9/27, 9/29 Inductively defined propositions; Maps SF book: IndProp and Maps chapters HW6 due on Oct 5th
Week 7 10/4, 10/6 The IMP language SF book: Imp chapter HW7 due on Oct 12th
Week 8 10/11, 10/13 Program equivalence; small-step operational semantics SF book: Equiv and Smallstep chapters HW8 due on Oct 19th
Week 9 10/18 Paper presentation by Rob Smith Xavier Leroy. Formal verification of a realistic compiler.
10/20 Small-step operational semantics SF book: Smallstep chapter HW9 due on Nov 2nd
Week 10 10/25, 10/27 Cancelled; instructor on academic travel
Week 11 11/1 Paper presentation by Ashley Huhman Beringer, Petcher, Ye, and Appel. Verified correctness and security of OpenSSL HMAC.
11/3 Types SF book: Types chapter HW10 due on Nov 9th
Week 12 11/8 Paper presentation by Dongrui Zeng Morrisett, Tan, Tassarotti, Tristan, and Gan. RockSalt: Better, Faster, Stronger SFI for the x86.
11/10 Dataflow analysis Principle of Program Analysis: chapter 2
Week 13 11/15, 11/17 Dataflow analysis Principle of Program Analysis: chapter 2 HW11 due on Nov 23rd
Week 14 11/22, 11/24 Thanksgiving break Thank you!
Week 15 11/29 Paper presentation by Shen Liu Zhao, Nagarakatte, Martin, and Zdancewic. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. POPL 2012.
12/1 Interprocedural analysis Principle of Program Analysis: chapter 2
Week 16 12/6 Interprocedural analysis
12/8 Student final project presentations