Undergraduate Course: Formal Verification (INFR11129)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Credit level (Normal year taken) | SCQF Level 11 (Year 4 Undergraduate) |
Availability | Available to all students |
| SCQF Credits | 10 |
ECTS Credits | 5 |
| 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
|
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-requisites | See above. |
| High Demand Course? |
Yes |
Course Delivery Information
| Not being delivered |
Learning Outcomes
On completion of this course, the student will be able to:
- Deploy bounded and unbounded model checking techniques to formally verify temporal logic properties of digital hardware and other finite state systems and protocols,
- Use an assertion-based software formal-verification tool to verify desired properties of computer programs,
- Describe the basic mechanics of SAT/SMT solvers and explain how they can be applied to discharge verification queries.
- 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. |
| Keywords | Hardware verification,Formal verification,Software verification,Model checking,SMT,SAT,BDD,Assertion |
Contacts
| Course organiser | Dr Elizabeth Polgreen
Tel:
Email: elizabeth.polgreen@ed.ac.uk |
Course secretary | Miss Lori Anderson
Tel: (0131 6)51 4164
Email: lori.anderson@ed.ac.uk |
|
|
University Homepage