Lecture Notes

Week 1: Introduction to Algorithmic Verification. Intro1, Intro2 (updated)
Week 2: Automata Theory 101. Automata (full set of slides)
Week 3: Temporal Logic. Logic (full set of slides)
Week 4: CTL Model Checking. CTL MC 1, CTL MC 2
Week 5: Symbolic Model Checking and NuSMV. Symbolic MC, NuSMV
Week 6: Tools: NuSMV and SPIN. SPIN, NuSMV code, apprentice (with mistakes), apprentice2 (correct)
Week 7: LTL Model Checking. LTL MC, LTL to Buchi
Week 8: Partial Order Reduction. POR
Week 9: SAT Solving, Bounded Model Checking, Abstraction Refinement. SAT/BMC, Refinement
Week 10: Data Flow Analysis, Abstract Interpretation. Static Analysis
Week 11: Real-time Systems I. Timed Automata, Regions
Week 12: Real-time Systems II. Zones, Hybrid Systems