THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2020/2021

Information in the Degree Programme Tables may still be subject to change in response to Covid-19

University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Undergraduate Course: Formal Verification (INFR11129)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Credit level (Normal year taken)SCQF Level 11 (Year 4 Undergraduate) AvailabilityAvailable to all students
SCQF Credits10 ECTS Credits5
SummaryFormal 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
*Software model checking, focusing on its use for finding concurrency bugs
*Pattern-based detection of concurrency bugs

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
Entry Requirements (not applicable to Visiting Students)
Pre-requisites Co-requisites
Prohibited Combinations Other requirements Incoming students are expected to be familiar with discrete maths at a level similar to that taught in the School of Informatics course Discrete Mathematics and Mathematical Reasoning (INFR08023). Prior exposure to predicate logic is also helpful. Programming experience in an imperative language such as Java, C or C++ is also essential for handling the material related to software verification.

For the hardware verification aspects of the course, prior exposure to hardware design is not needed, but students do need to be familiar with Finite-State Automata concepts.
Information for Visiting Students
Pre-requisitesSee above.
High Demand Course? Yes
Course Delivery Information
Not being delivered
Learning Outcomes
On completion of this course, the student will be able to:
  1. Deploy bounded and unbounded model checking techniques to formally verify temporal logic properties of digital hardware and other finite state systems and protocols,
  2. Use an assertion-based software formal-verification tool to verify desired properties of computer programs,
  3. Describe formal techniques that can be used for the detection of concurrency bugs in software,
  4. Assess the pros and cons of using different automated formal verification approaches on a previously-unseen hardware or software system.
Reading List
- Logic in Computer Science (2nd Ed).why3 Huth and Ryan. Cambridge UP. 2004.
- NuSMV model checker documentation and tutorials. http://nusmv.fbk.eu/
- SPARK toolset documentation and training materials. https://www.adacore.com/about-spark
- Why3 programme verification toolkit documentation and tutorials. http://why3.lri.fr
- CBMC (Bounded model checker for C and C++) documentation, http://www.cprover.org/cbmc/.
Additional Information
Graduate Attributes and Skills - Apply critical analysis, evaluation and synthesis to forefront issues, or issues that are informed by forefront developments in the subject/discipline/sector.
- Critically review, consolidate and extend knowledge, skills, practices and thinking in a subject/discipline/sector.
- Deal with complex issues and make informed judgements in situations in the absence of complete or consistent data/information.
- Communicate with peers, more senior colleagues and specialists.
- Use a wide range of ICT applications to support and enhance work at this level and adjust features to suit purpose.
KeywordsHardware verification,Formal verification,Software verification,Model checking,SMT,SAT,BDD,Assertion
Contacts
Course organiserDr Paul Jackson
Tel: (0131 6)50 5131
Email: Paul.Jackson@ed.ac.uk
Course secretaryMiss Clara Fraser
Tel: (0131 6)51 4164
Email: clara.fraser@ed.ac.uk
Navigation
Help & Information
Home
Introduction
Glossary
Search DPTs and Courses
Regulations
Regulations
Degree Programmes
Introduction
Browse DPTs
Courses
Introduction
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Combined Course Timetable
Prospectuses
Important Information