FV: Formal Verification

Welcome to Formal Verification

Hello, welcome to the 2023-24 run of Formal Verification. 

The course this year is taught by Paul Jackson. 

On this page:

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

For a more detailed overview, see the Course Description below or the DRPS Course Descriptor.

Lectures

Lecture are in Semester 1 at 15:10-16:00 in Weeks 1 to 11:

  • Mondays in Appleton Tower, Room 2.12,
  • Thursdays in Appleton Tower, Lecture Theatre 3.

The first lecture is on Monday 18th September 2023.  

Not every lecture time will be used: see the Course Schedule for details. 

Labs

Drop-in lab sessions are at 11:10-13:00 in Weeks 3 to 10 in Appleton Tower, Room 4.12.  At each lab session the course lecturer and/or the course demonstrator will be available to answer questions about lecture material, practical exercises and coursework.

Courseworks

Two courseworks are planned. See the course Learn pages for further information on these courseworks.  

Practical Exercises

Through the course, several exercises will be released in the use of various formal verification tools.   While these exercises are not formally assessed, you are strongly encouraged to work through them.  Sometimes, they will lead in to coursework involving the same tools.  They also will broaden your experience of formal verification tools.   If you like, you can work on the exercises in pairs.  Solutions to the exercises will be released.

Seeking Help

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, you can:

  • post questions on the course's Piazza discussion forum,
  • ask questions at one of the drop-in lab sessions,
  • email the course lecturer Paul Jackson.

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, practical exercises, and courseworks.

Further Reading

The course lecture slides are designed to be reasonably self-contained.  When appropriate, links are provided on the Schedule page to further information on the topics covered in lectures.  

On the course's Learn page, near the foot of the Content section, is a link to a Library Resources page which in turn links to a Resource List, the University Library's online reading list tool.   This tool displays information on recommended books and books for further reading.  When the Library has online access to a book, it links to the online version.  In some cases, the Library has physical copies and a library catalogue code is given to help you locate the book. You are encouraged to have a browse, particularly of introductory sections in these books.  However, do note that these books go far far beyond what you are expected to know for the course assessments.

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  
     

Possible further topics include the following:

  • 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
License
All rights reserved The University of Edinburgh