</a></b></td>

Date | Type | Unit | Material |
---|---|---|---|

8/29 | Lecture | L0 | Course Intro and Propositional Logic (Slides) |

8/31 | Lecture | L1 | Finishing L0; Intuitionistic Propositional Logic (Part 1) (Slides) |

9/5 | Lecture | L2 | Kris gone at ICFP '23, class canceled |

9/7 | Lecture | L3 | Intuitionistic Propositional Logic (Slides) |

9/12 | Lecture | L4 | Propositional Resolution and DPLL (Slides) |

9/14 | Lecture | L5 | DPLL paper discussion |

9/14 | Project | P1 | SAT Solving -- Released (Slides/Specification) |

9/19 | Lecture | L6 | Conflict-Directed Clause Learning (Reading) (Slides) |

9/21 | Lecture | L7 | Chaff: Engineering an Efficient SAT Solver |

9/26 | Lecture | L8 | Learning in CDCL; Horn-SAT and Datalog |

9/28 | Lecture | L9 | An Extensible SAT-solver |

9/28 | Project | P1 | PROJECT 1 DEADLINE |

9/28 | Project | P2 | Implementing Datalog -- Released (click me!) |

10/3 | Lecture | L11 | Datalog Implementation; First-Order Logic and SMT primer |

10/5 | Lecture | L11 | Automatic Index Selection for Large-Scale Datalog Computation |

10/10 | Fall Break | ||

10/12 | Lecture | L12 | EXE: Automatically Generating Inputs of Death |

10/12 | Project | P2 | PROJECT 2 DEADLINE |

10/17 | Lecture | L13 | Satisfiability Modulo Theories (SMT); uninterpreted functions and bitvectors |

10/17 | Project | P3 | Symbolic Executor -- Released |

10/19 | Lecture | L14 | Solving uninterpreted functions via union-find; Steensgaard analysis |

10/24 | Lecture | L15 | Extending Datalog to Recursive Aggregation (led by Yihao) |

10/26 | Exam | M1 | Bonus Take-Home Midterm 1 (no class!) |

10/31 | Lecture | L16 | Solving combined first-order theories; DPLL(T) |

11/2 | Lecture | L17 | (Kris Gone): Meet to work on P3 |

11/7 | Lecture | L18 | Strucured Datalog and Slog |

11/9 | Lecture | L19 | Higher-Order, Data-Parallel Structured Deduction |

11/9 | Project | P3 | PROJECT 3 DEADLINE |

11/9 | Project | P4 | Final Project: Prepare a Lecture -- Released |

11/14 | Lecture | L20 | Model Checking, Buchi Automata, LTL and CTL |

11/16 | Lecture | L21 | Software Model Checking |

11/21 | Thanksgiving Break (Tu) | ||

11/23 | Thanksgiving Break (Th) | ||

11/28 | Lecture | L22 | Generalized Property-Directed Reachability |

11/30 | Lecture | L23 | Student Group Lectures -- Day 1 |

12/5 | Lecture | L24 | Student Group Lectures -- Day 2 |

12/7 | Lecture | L25 | Student Group Lectures -- Day 3 |

Final | Final Project (Detailed Notes and Slides) -- Due |