Formal Verification (2017-18)

THIS COURSE IS NOT RUNNING IN THE 2018-19 ACADEMIC YEAR

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.

Please see the DRPS course descriptor or the Path version of the course descriptor for a fuller description of the content of the course. Also Informatics provide a course summary.

On this page:

Staff

Lecturers:

Course TA: Jake Palmer. Email: s1673264@sms.ed.ac.uk.

Lab demonstrator: Jake Palmer.

Help and Feedback

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.

Labs

Lab sessions are held in 4.12, Appleton Tower between 11.10 and 13.00 on Wednesday. The lab sessions will start in Week 3, with no lab during the mid-semester break (19-23 Feb). At each lab session at least one of the course TAs, lecturers and/or demonstrators will be available to help with any problems with course material and coursework.

Lecture Schedule

Lectures are held in Semester 2 at 16.10-17.00:

The first lecture is on Tuesday 16th January 2018.

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.

Week Date Title Recommended Reading
1 Tue 16 Jan 2018 Course Overview
1. Introduction to Model Checking and Temporal Logic
H&R Sections 3.1, 3.2
Fri 19 Jan 2018 2. Linear Temporal Logic H&R Section 3.2
2 Tue 23 Jan 2018 3. The NuSMV model checker H&R Section 3.3
NuSMV Start-up Guide
Fri 26 Jan 2018 4. Practical Exercise See the Practical files
3 Tue 30 Jan 2018 5. Computation Tree Logic H&R Sections 3.4, 3.5, 3.6.1 and 3.7
Fri 2 Feb 2018 6. How LTL Model Checking Works
ltl-mc.smv
H&R Sections 3.6.2 and 3.6.3
4 Tue 6 Feb 2018 7. Introduction to Binary Decision Diagrams (BDDs) H&R Section 6.1
[background] An Introduction to Binary Decision Diagrams by Henrik Reif Andersen.
Fri 9 Feb 2018 8. Operations on BDDs H&R Sections 6.2, 6.3
5 Tue 13 Feb 2018 9. No Lecture
Fri 16 Feb 2018 10. Discussion of the (Solutions to the) Practical Exercise See the handouts and some of the solutions already posted on the class discussion forum
  Tue 20 Feb 2018 Mid-Semester Break (no lecture)
Fri 23 Feb 2018 Mid-Semester Break (no lecture)
6 Tue 27 Feb 2018 11. Introduction to second half of course
SPARK verification features - Part 1
Fri 2 Mar 2018 12. SPARK verification features - Part 2
7 Tue 6 Mar 2018 13. SPARK verification features - Part 3
Fri 9 Mar 2018 14. Programming language semantics Concrete Semantics by Nipkow and Klein: Sections 7.1, 7.2 and 12.4.
8 Tue 13 Mar 2018 15. SPARK tool-set Tutorial and video on Z3 SMT Solver and SMTLIB language
Why3 homepage
Why3 gallery
Fri 16 Mar 2018 16. WP-based methodology and tools
9 Tue 20 Mar 2018 17. Software bounded model checking with CBMC 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
Fri 23 Mar 2018 18. SAT algorithms
10 Tue 27 Mar 2018 19. Guest Lecture: Industrial applications of static verification. Rod Chapman
Fri 30 Mar 2018 20. SAT & SMT algorithms
11 Tue 3 Apr 2018 21. Exam review for software verification material and 2017 past paper For exam questions on model checking see past papers from old Automated Reasoning course:
2011-12
2012-13
2013-14
2014-15

and the Formal Verification past paper:
2016-17
Fri 6 Apr 2018 22. No Lecture

Assessment and Coursework

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.

Exercise 1
The first practical exercise involves model checking using NuSMV.
Additional exercises
The LTL and CTL exercises are the same except for an extra example this year.
Exercises 2 & 3
For the first and second labs on checking assertions in the SPARK language, visit the SPARK lab page.
Exercise 4
For this exercise introducing the CBMC bounded model checker for C, visit the CBMC lab page.

Formal Verification Tools

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.


Home : Teaching : Courses 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh