Date

Topic

Assignment Released

06/02

Intro

A1

06/03

• Dafny Basics

• Getting Started with Dafny

06/05

Floyd Hoare Logic

06/08

Hoare Triple

Quiz 1

06/10

Inductive Proofs

06/12

Inductive Proofs

A2

06/15

Inductive Types

Quiz 2

06/17

• Inductive Types

• Sorting

06/18

• Hoare Triple: Loops

• Loop Invariants

06/19

• Arrays

• SAT Solver Basics

A3

06/22

SAT Solvers

Quiz 3

06/24

Solving SAT and SMT Problems Using Z3

06/26

DPLL and CDCL Algorithms

06/29

DPLL and CDCL Algorithms

06/30

• Testing

• Symbolic Execution

07/01

Midterm Review

A4

07/02

Midterm Exam

07/03

Concolic Execution

07/06

• Functional Programming in Rocq

• source code

Quiz 4

07/08

• Logic in Rocq

• source code

07/10

• Logic in Rocq

• source code

Quiz 5

07/13

• Induction in Rocq

• source code

A5

07/15

• Induction in Rocq

• source code

07/17

• Basic Program Syntax

• source code