Lectures

	Lecture 1: Intro
	Lecture 2: Logistics, Specifications in LSL
	Lecture 3: Propositional Logic in Code
	Lecture 4: Using LSL
	Lecture 5: Design / Specification Recipe
	Lecture 6: Using LSL II
	Lecture 7: Using LSL III
	Lecture 8: Relational Specifications
	Lecture 9: Dependent Contracts
	Lecture 10: Itemizations
	Exam 1
	Lecture 12: Recursive Contracts
	Lecture 13: More Recursive Data
	Lecture 14: Continuing with Recursive Data
	Lecture 15: Specifications with Functions
	Lecture 16: Polymorphism
	Lecture 17: Polymorphism II
	Lecture 18: Programming Against Interfaces
	Lecture 19: Finitizing, Rosette
	Lecture 20: Recursion & Induction
	Lecture 21: Temporal Specifications
	Exam 2
	Lecture 23: Reasoning about Mutable State
	Lecture 24: Value Mutation
	Lecture 25: More Pointer Equality
	Lecture 26: Concurrency
	Lecture 27: Concurrency II
	Lecture 28: Concurrency Lab
	Lecture 29: Big-O
	Lecture 30: More Performance
	Lecture 31: Visualization for Concurrency
	Lecture 32: Resources
	Lecture 33: Introduction to Proof
	Lecture 34: Proofs with Propositional Logic
	Lecture 35: Proofs with Tactics
	Exam 3
	Lecture 37: Inductive types/ proofs, Proof automation
	Lecture 38: LLMs & Specification

8.11