CS 576: Topics in Automated Deduction (Spring 2026): Lectures main  ::  policy  ::  lectures  ::  mps  ::  project  ::  faq  ::  doc  ::  downloads

Videos of class lectures Lecture Schedule for Spring 2026 Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Jan 20 Course Introduction slides (full sized PDF) (six up PDF) files Demo1.thy files Demo2_inc.thy Jan 22 Intro continued slides (full sized PDF) (six up PDF)   Jan 27 Basic Isabelle syntax slides (revised) (full sized PDF) (six up PDF) Jan 29 Introducing new types and terms slides (full sized PDF) (six up PDF) files Demo3.thy   Feb 3 Datatypes slides (full sized PDF) (six up PDF) files Demo4.thy Feb 5 Function Definitions slides (full sized PDF) (six up PDF) files Demo4.thy files Demo5.thy   Feb 10 Rewriting slides (full sized PDF) (six up PDF) Feb 12 Introduction and Elimination Rules in HOL (cont) slides (full sized PDF) (six up PDF) files Demo6.thy   Feb 17 Quantifier Intro and Elim Rules in HOL slides (full sized PDF) (six up PDF) files Demo7.thy Feb 19 Basic Proof Methods slides (full sized PDF) (six up PDF) files Demo7.thy   Feb 24 Intro to Set Theory, Inductive Sets slides (full sized PDF) (six up PDF) files Demo8.thy Feb 26 Inductive Sets cont, Inductive Relations slides (full sized PDF) (six up PDF) files Demo9.thy   Mar 3 New Type Definitions, Records slides (full sized PDF) (six up PDF) files Demo10.thy, Demo11.thy Mar 5 Locales slides (full sized PDF) (six up PDF) files Demo12.thy   Mar 10 Example development: CTL slides 15-ctl-spec.html files 15/Demo12.thy 15/Paths.thy 15/ctl_syntax.thy Mar 12 Example development: CTL (cont) Slides and theory devlopment continued from March 10   Mar 17 SPRING BREAK Mar 19 SPRING BREAK   Mar 24 Example development: CTL (cont) slides 17/17-ctl-spec.html files 17/Demo12.thy 17/Paths.thy 17/ctl_syntax.thy Mar 26 Example development: CTL (cont) files 18/Demo12.thy 18/Paths.thy 18/ctl_semantics.thy 18/ctl_syntax.thy   Mar 31 Example development: CTL (cont) slides 19/19-ctl-models.html files 19/TransitionSystem.thy 19/Paths.thy 19/ctl_semantics.thy 19/ctl_syntax.thy Apr 2 Example development: CTL (cont)   Apr 7 Example development: CTL (cont) slides 21/21-projects-and_ctl-models.html files 21/Paths.thy 21/TransitionSystem.thy 21/ctl_semantics.thy 21/ctl_syntax.thy Apr 9   Preliminary Problem Statement in Isabelle   Student's name   Topic   Elsa Gunter   Formal Verfication of a CTL Model Checker   Nancy Jia   Formalization of Graph Burning with Isabelle   Ross Sponholtz   Impossibility of Leader Election in Anonymous Synchronous Rings               Apr 14   Preliminary Problem Statement in Isabelle   Student's name   Topic   Kenneth Hunter   Validation of Simplex I2C Protocol for Embedded Systems   Aryan Arora   Formal Verification in Quantum Computing   Nausheen Mohammed   Soundness of a Rely-Guarantee-based Proof System for Relational Program Verification   Saadat Kamaei   Formal Verification of Constant Folding   Stanley Yang   Proving the Dijkstra's Algorithm in Isabelle     Apr 16   Preliminary Problem Statement in Isabelle   Student's name   Topic   Akhil Isanaka   Semantic Equivalence of Constant Folding   Shaw Kagawa   Formalization of parts of global string alignment for sequence alignment   Daniel Kwan   Formalization of a SLO-Aware Scheduling Algorithm for LLM Serving   Gabriel Warner   IoT authentication protocol   Noah Zheutlin   Solved Games   Mark Chen   Formal Verification of Breadth-First Search (BFS)   Apr 21   Preliminary Problem Statement in Isabelle   Stuti Agrawal   Formal Verification of the Viterbi Algorithm for Hidden Markov Models (HMMs)     Apr 23   Apr 28 April 30   May 5