On this page:
Please register your feedback on this course at the Informatics Course Survey.
The lectures are given by:
If you run into difficulties and are not making satisfactory progress then seek help. The earlier you ask for help the more likely it is that your problems can be solved without damaging your performance in the course. Do not be ashamed of asking for help. This is a challenging course, which introduces you to novel techniques and skills. You are expected to learn them during the course, not to come already equipped with them.
To seek help
Even if you are managing fine, please feel free to use the discussion forum to ask questions on course-related topics that go beyond the core material presented in the lectures and courseworks.
Various kinds of feedback are provided during the course.
Lectures are held at 16.10-17.00 in Semester 2 on Tuesdays and Fridays in LG34 of Paterson's Land.
The first lecture is on Tuesday 12th January 2016.
Note that there are no lecture notes for the course. Instead, recommended reading is associated with each lecture. This reading is usually from:
There will be one lecture on each of the coursework assignments to provide some general information and background. Note: These lectures do not necessarily coincide with the hand-out dates for the assignment sheets. Students should start work on their courseworks as soon as they are handed out rather than wait for the lectures, if these come later on.
Please note: At any point of the course, the future schedule gives a strong indication of the topics to be covered. However, some details might change.
|1||Tue 12th Jan 2016||1. Introduction||Bundy, Ch. 1
[background] The Univalent Foundations presentation by Vladimir Voevodsky.
|Fri 15th Jan 2016||2. Propositional Logic and Natural Deduction
|H&R Sec 1.1, 1.2, 1.3, start of 1.4
[background] Wadler's Propositions as Types
|2||Tue 19th Jan 2016||3. Natural Deduction and Starting with Isabelle
|H&R Sec 1.2, 1.4
Getting Started with Isabelle
Sec 5.1-5.7 of Tutorial on Isabelle/HOL
Prop.thy Isabelle theory file
|Fri 22nd Jan 2016||4. Propositional Reasoning in Isabelle
Sec 5.1-5.7 of Tutorial
[background] Pollack's How to Believe a Machine-Checked Proof
[background] How do they verify a verifier of formalized proofs?
|3||Tue 26th Jan 2016||5. First-order Logic
H&R Secs 2.1-2.4
FOL.thy Isabelle theory file
[background] Logitext - an interactive L-system FOL prover
|Fri 29th Jan 2016||6. Representation & Introduction to HOL
|Bundy Ch. 4|
|4||Tue 2nd Feb 2016||7. Coursework 1: Proving and Reasoning in Isabelle/HOL
Note: The coursework has been updated on 9 February!— Coursework description
— Coursework theory file
|Fri 5th Feb 2016||8. Unification
|Bundy 17.1 - 17.4
[background] Unification theory -- a survey of the state of the art from 2001.
|5||Tue 9th Feb 2016||9. Rewriting
|Bundy Ch. 9|
|Fri 12th Feb 2016||10. Guest Lecture: Ewen Maclean - Creativity in Inductive Theorem Proving
|Bundy Ch. 11
[background] Productive Use of Failure in Inductive Proof
|Tue 16th Feb 2016||Innovative Learning Week (no lecture)|
|Fri 19th Feb 2016||Innovative Learning Week (no lecture)|
|6||Tue 23rd Feb 2016||11. Formal Verification and Linear-time Temporal Logic||H&R Sections 3.1, 3.2|
|Fri 26th Feb 2016||12. Linear Temporal Logic, continued
(same slide set as last lecture)
|H&R Section 3.2|
|7||Tue 1st Mar 2016||13. The NuSMV model checker
||H&R Section 3.3
NuSMV Start-up Guide
|Fri 4th Mar 2016||14. Coursework 2|
|8||Tue 8th Mar 2016||15. Computation Tree Logic||H&R Sections 3.4, 3.5|
|Fri 11th Mar 2016||16. LTL Model Checking Idea
|H&R Sections 3.6.2 and 3.6.3|
|9||Tue 15th Mar 2016||17. CTL Model Checking||H&R Sections 3.6.1, and 3.7|
|Fri 18th Mar 2016||18. Introduction to Binary Decision Diagrams (BDDs)||H&R Section 6.1
[background] An Introduction to Binary Decision Diagrams by Henrik Reif Andersen.
|10||Tue 22nd Mar 2016||19. Operations on BDDs||H&R Sections 6.2, 6.3|
|Fri 25th Mar 2016||20. Software model checking
| Slides on CBMC
Slides on BLAST
|11||Tue 29th Mar 2016||21. Exam Review||
Older (contain material not in the current course):
|Fri 1st Apr 2016||22. No Lecture|
There are two pieces of software that we will be using for this course.
The Isabelle2015 theorem prover. Isabelle should be installable on your own computer by following the instructions on the linked webpage.
To run Isabelle on the DICE machines in the labs, run the following command from the terminal: Isabelle
More information about using Isabelle is available in the Isabelle Startup Guide.
There is also a Cheat sheet listing common Isabelle proof commands and rules.
The NuSMV model checker. This will be used in the second half of the course, and is also installed on DICE.
Information about using NuSMV is available in the NuSMV Startup Guide
There will be two items of assessed coursework for this course, both of which count for 20% of the overall mark (the other 60% is assessed by exam).
The dates for the coursework are as follows:
The first coursework overlaps with Innovative Learning Week, which accounts for the longer elapsed time between hand out and deadline.
Hand out: 2nd February 2016. Deadline: 4pm, Friday 26th February 2016.
Note: Coursework 1 has been updated on 9 February!
Coursework 2: Hand out 4th March 2016 (Week 7). Deadline: Friday 18th March 2016 at 4pm(Week 9)
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: firstname.lastname@example.org
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh