Schedule

Date Topics Reading Assignments
08/26 Introduction
08/28 Software Testing Semantic Fuzzing with Zest P1 (Due: 09/12)
09/02 Labor day, No class
09/04 Programming in Dafny notes code Program Proofs: Chapter 6
09/09 Arrays, Sequences, Sets, and Searching code
Annotating Dafny Programs 		Program Proofs: Chapter 13
09/11 Hoare Logic, code, in class examples Program Proofs: Chapter 2, paper:An Axiomatic Basis for Computer Programming
09/16 Hoare Logic: Loops, code, in class examples Program Proofs: Chapter 11 P2 (Due: 09/30)
09/18 Sorting, in class examples Program Proofs: Chapter 15 Quiz 1
09/23 SAT Solver Basics
09/25 DPLL and CDCL
09/30 Z3 API in Python
 Z3 API in Python Quiz 2
10/02 Guest Lecture: Mike Hicks Verification-Guided Development (VGD)
10/07 More Python Z3
 P3 (Due: 10/18)
10/09 Symbolic Execution
10/14 Preface.v Basics.v
_CoqProject 		Coq: Preface
Coq: Basics
10/16 Induction.v
Makefile 		Induction P4: (Due 11/07)
10/21 Midterm Review
10/23 Midterm Exam
10/28 Lists.v
Makefile 		Lists P4 Part 2:(Due 11/07)
10/30 Poly.v
Makefile 		Poly
11/04 Tactics.v
Makefile 		Tactics
11/06 Logic.v
Makefile 		Logic P5 Part 1:(Due 11/22)
11/11 Logic.v
Makefile 		Logic Quiz 3
11/13 IndProp.v
Makefile 		IndProp
11/18 Concurrency
11/20 Concurrency cont.
 Final Project:(Due 12/09)
12/02 Concurrency cont. (ForkJoinPool, Actor Model)
12/04 Concurrency cont. (Parallel Streams, Map/Reduce)