Formal verification is the use of mathematical techniques to verify the correctness of various kinds of engineering systems: software systems and digital hardware systems, for example. Formal verification techniques are exhaustive and provide much stronger guarantees of correctness than testing or simulation-based approaches. They are particularly useful for safety and security critical systems and for when system behaviour is highly complex. They are also now being used for some commercial software when bugs have a major impact on customer satisfaction. The course focuses on automated techniques that are currently used in industry. It gives practical exposure to current formal verification tools, explaining the input languages used and introducing the underlying mathematical techniques and algorithms used for automation.
This is a new course for 2016-17. New material on software verification is being developed.
On this page:
Lab demonstrators: Daniel Raggi (First Part)
Course TA: Daniel Raggi (First Part)
Lectures are held at 16.10-17.00 in Semester 2 on Tuesdays and Fridays in Room 2.13 of Old Infirmary (Geography), 1 Drummond Street, Edinburgh EH8 9XP.
The first lecture is on Tuesday 17th January 2017.
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 formative, non-assessed practical exercises to provide some general information and background. Note: These lectures do not necessarily coincide with the hand-out dates for the practical sheets. Students should start work on their exercises soon as they are handed out rather than wait for the lectures, if these come later on.
|1||Tue 17 Jan 2017|| — Course Overview
1. Introduction to Model Checking and Temporal Logic
|H&R Sections 3.1, 3.2|
|Fri 20 Jan 2017||2. Linear Temporal Logic||H&R Section 3.2|
|2||Tue 24 Jan 2017||3. The NuSMV model checker||H&R Section 3.3
NuSMV Start-up Guide
|Fri 27 Jan 2017||4. Practical Exercise||See the Practical files|
|3||Tue 31 Jan 2017||5. Computation Tree Logic||H&R Sections 3.4, 3.5, 3.6.1 and 3.7|
|Fri 3 Feb 2017||6. How LTL Model Checking Works
|H&R Sections 3.6.2 and 3.6.3|
|4||Tue 7 Feb 2017||7. Introduction to Binary Decision Diagrams (BDDs)||
H&R Section 6.1
[background] An Introduction to Binary Decision Diagrams by Henrik Reif Andersen.
|Fri 10 Feb 2017||8. Operations on BDDs||H&R Sections 6.2, 6.3|
|5||Tue 14 Feb 2017||9. Discussion of the (Solutions to the) Practical Exercise||See the handouts and some of the solutions already posted on the class class discussion forum|
|Fri 17 Feb 2017||10. No Lecture
|Tue 21 Feb 2017||Mid-Semester Break (no lecture)|
|Fri 24 Feb 2017||Mid-Semester Break (no lecture)|
|6||Tue 28 Feb 2017||11. No Lecture|
|Fri 3 Mar 2017||12. Introduction to second
half of course
SPARK verification features - Part 1
|7||Tue 7 Mar 2017||13. SPARK verification features - Part 2|
|Fri 10 Mar 2017||14. SPARK verification features - Part 3|
|8||Tue 14 Mar 2017||15. Programming language semantics||Concrete Semantics by Nipkow and Klein: Sections 7.1, 7.2 and 12.4.|
|Fri 17 Mar 2017||16. SPARK tool-set||
Tutorial and video
on Z3 SMT Solver and SMTLIB language
|9||Tue 21 Mar 2017||17. WP-based methodology and tools|
|Fri 24 Mar 2017||18. SAT algorithms|
|10||Tue 28 Mar 2017||19. SAT & SMT algorithms|
|Fri 31 Mar 2017||20. Software bounded model checking with CBMC||
Bounded Model Checking for ANSI-C An introduction to CBMC.
The CProver Suite of Verification Tools. Martin Brain. First part of a tutorial given at the FM 2016 conference
|11||Tue 4 Apr 2017||21. Exam review for software verification material||
For exam questions on model checking see past papers from old Automated Reasoning course:
|Fri 7 Apr 2017||22. No Lecture|
Assessment is 100% based on a final exam. Several formative non-assessed practical exercises will be provided to give you familiarity with formal verification tools and help you better understand formal verification techniques. Demonstrators and your peers on the course will review your solutions to exercises and the lecturers will introduce the exercises and provide notes on the solutions.
Several formal verification tools will be used on this course. A possible set of tools is as follows. This set might well change as the course unfolds.
The SPARK toolset from Altran UK for the verification of programs written in the SPARK subset of Ada.
CBMC, a bounded model checker for C and C++.
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 shy 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.
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