FV: Schedule
In the schedule information below
- Lecture slides are linked to from the lecture titles
- "H&R" refers to the book by Michael Huth and Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd Edition, Cambridge University Press, 2004. See the Further Reading section on the course's OpenCourse home page for how to navigate to online editions of this book and other books relevant to the course.
- The plan for future lectures is provisional and might change as the semester progresses.
| Week | Date | Lecture | Further Information |
|---|---|---|---|
| 1 | Mon 18 Sep 2023 | 1a. Course Introduction 1b. Model Checking Overview | H&R Sections 3.1, 3.2 |
| Thu 21 Sep 2023 | 2. Linear Temporal Logic | H&R Section 3.2 | |
| 2 | Mon 25 Sep 2023 | 3. Computation Tree Logic | H&R Sections 3.4, 3.5 Moshe Vardi. Branching vs. Linear Time: Final Showdown. TACAS 2001 |
| Thu 28 Sep 2023 | 4. The NuXmv model checker | Getting started with NuSMV & nuXmv nusmv-examples.zip | |
| 3 | Mon 2 Oct 2023 | 5. How CTL Model Checking Works | H&R Sections 3.6.1, 3.6.2, 3.7 |
| Thu 5 Oct 2023 | NO LECTURE | ||
| 4 | Mon 9 Oct 2023 | 6. How LTL Model Checking Works | H&R Sections 3.6.2, 3.6.3 CW1 Handout |
| Thu 12 Oct 2023 | 7. Introduction to BDDs | H&R Section 6.1 | |
| 5 | Mon 16 Oct 2023 | 8. BDD Operations | H&R Sections 6.2, 6.3 |
| Thu 19 Oct 2023 | 9. SAT & SMT solving | See last page of slides | |
| 6 | Mon 23 Oct 2023 | 10. SAT & SMT solving (Slides from Lecture 9) | 12 Noon - CW1 Handin |
| Thu 26 Oct 2023 | 11a. SPARK Introduction 11b. Verification with SPARK | Practical Exercise 2: SAT&SMT with Z3 | |
| 7 | Mon 30 Oct 2023 | 12. Verification with SPARK 2 (Slides from Lecture 11b) | |
| Thu 2 Nov 2023 | NO LECTURE | Practical Exercise 3: Verification with SPARK | |
| 8 | Mon 6 Nov 2023 | 13. Verification with SPARK 3 (Slides from Lecture 11b) | CW2 Handout |
| Thu 9 Nov 2023 | 14. Programming Language Semantics | See last page of slides | |
| 9 | Mon 13 Nov 2023 | 15. SPARK tool architecture and other similar tools | Follow links on slides |
| Thu 16 Nov 2023 | 16. FV - The Big Picture | Follow links on slides | |
| 10 | Mon 20 Nov 2023 | 17. Bounded Model Checking for C | 12 Noon - CW2 Handin For more about CBMC, follow the link below. |
| Thu 23 Nov 2023 | NO LECTURE | Practical Exercise 4: Verification with CBMC | |
| 11 | Mon 27 Nov 2023 | NO LECTURE | |
| Thu 30 Nov 2023 | NO LECTURE |
License
All rights reserved The University of Edinburgh