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.

The lecture videos were recorded about 4 years ago. As such, certain things (for instance the specific demonstrations with the theorem prover Dafny) are a bit out-of-date, because the newer version of the tool behaves slightly differently. Nevertheless, the tool is just a presentation aid, and the main concepts are always the same and remain the same forever. Hence, you can still take advantage of the videos for learning those concepts. The updated Dafny files that work with the current verison will be posted together with the rest of the lecture material.

• Week (1): Introduction to the course and program correctness
  • Introduction
  • GCD1
  • GCD2
  • GCD correctness
    • Proof does not work with your Dafny version? See here.
• 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