Lecture Videos

You will find lecture slides posted here. These videos provide a compact introduction to the course material. During the synchronous (in-person) class, we will do exmaples, answer questions, and discuss extended material that help with a good command of this material. This will give us the opportunity to dig deeper into each concept through extended examples in an interactive class. We will not repeat the matrial from the videos in the synchronous class. It will be a waste of everyone's time. It is your resposnibility to watch the relevant videos in advance of each class.

• Week (1): Introduction to the course and program correctness
  • Introduction
  • GCD1
  • GCD2
  • GCD correctness
• Week (2): Program Correctness
  • Introduction part 2
  • Inductive Assertion Method
  • Find
  • Quotient/Remainder
  • Strengthening
  • Robot
• Week (3): Program Correctness
  • Partition
  • Partial Correctness
  • Recursive Robot
  • Termination
• Week (4,5): Dataflow Analysis
  • Introduction to Dataflow Analysis
  • The mathematics behind it
    • Part 1
    • Part 2
    • Part 3
  • Both sets of videos are external and are here for completeness. We will cover the material in more traditional lecture format together in class.
• Week (6): SAT
  • Intro
  • SAT Solving
  • DPLL Overview
  • Confict Driven Clause Learning
• Week (7): SMT
  • Equality Logic with Uninterpreted Functions
  • Linear Arithmetic
• Week (8): Symbolic Reachability
  • Classic Symbolic Reachability
  • Property-directed Reachability
• Week (9): Linear Temporal Logic
  • Introduction to Model Checking
  • Linear Temporal Logic
• Fall Break
• Week (10): Computation Tree Logic
  • LTL wrap up
  • Computational Tree Logic
• Week (11): CTL Model Checking:
  • video 1
  • video 2