Course finder

<< return to browsing

Semester 1

Formal Verification (INFR11129)

Course Website

http://course.inf.ed.ac.uk/fv/

Subject

Informatics

College

SCE

Credits

10

Normal Year Taken

4

Delivery Session Year

2023/2024

Pre-requisites

As above.

Course Summary

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. 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.

Course Description

In recent years there have been highly noteworthy cases of the adoption of formal verification (FV) techniques in industry. For example, at Intel, FV has largely replaced simulation-based verification of their microprocessors, at Microsoft, FV is used to certify that 3rd party drivers are free of certain kinds of concurrency bugs. As FV tools and methodologies improve, FV is expected to become more and more widely used in industry. This course aims to familiarise students with main classes of FV techniques that are likely to become most widespread in industry in the coming years. The intent is to prepare students who might go into industry with sufficient background in FV that they would be aware of when and how they might deploy FV techniques. The course will also be of interest to students who wish to go into research developing techniques for future-generation FV tools and who might need to use FV in their research. To satisfy these aims, the course has a practical focus, giving students hands-on experience with a number of tools and explaining their input languages for specifying systems and desired system properties. The course also introduces the underlying mathematical techniques, which gives students a deeper understanding of the tools and will help them use the tools most effectively. Topics the course covers include the following: *Formal verification in context, its current take-up in industry and challenges to its wider adoption *Syntax and semantics of CTL and LTL temporal logics *CTL and LTL model checking techniques, including automata-based approaches and bounded model checking with SAT solvers *The BDD data-structure used at the heart of many model checkers *Writing models for model checking and phrasing useful properties in CTL and LTL *Operational semantics of a simple imperative programming language, weakest precondition operators and verification condition generation *The capabilities of SMT solvers for discharging verification conditions *Assertion-based software verification Optional topics include: *Industrial temporal logics such as PSL and SVA used in hardware verification *Formal verification case studies *Formal verification of hybrid systems, system with both discrete state changes and continuous state changes governed by differential equations *Combining formal and simulation-based verification methods *Dual use of temporal logic properties and assertions in formal and simulation-based verification of hardware and software *Software model checking, focusing on its use for finding concurrency bugs *Pattern-based detection of concurrency bugs

Assessment Information

Written Exam 70%, Coursework 30%, Practical Exam 0%

Additional Assessment Information

Written Examination: 70%Coursework: 30%The course material is primarily introduced in lectures and assessment is by a final exam. Practical exercises are provided to give students familiarity with formal verification tools and help them better understand formal verification techniques. Support for students in using the tools is provided both by demonstrators in lab sessions and through the use of an online discussion forum. In addition, demonstrators review student solutions to exercises and the lecturer both introduces the exercises and presents model solutions.As the course focuses on the application of formal verification techniques, most exam questions will involve presenting various verification scenarios and exploring how verification techniques might be deployed in those scenarios. Often questions will focus on some particular aspect of a techniques, exploring for example how well students understand the input specification languages used by techniques. Other questions might involve students stepping through the behaviour of verification algorithms on small examples.

view the timetable and further details for this course