# CpSc 513: Introduction to Formal Verification

## Overview

Formal verification is the application of rigorous mathematical methods to show that hardware and software designs have the desired properties. The field is nearly as old as computers themselves, with some of the very earliest papers in computer science research exploring ways to use computers to prove mathematical theorems, and using mathematical methods to fight the pervasive problems of errors in hardware and software. Many of these ideas were well ahead of their time, and formal verification was largely an area of interest for logicians and theoretical computer scientists until the early 1990s. By the early 1990s, advances in algorithms and increased computing power made formal methods practical for hardware verification. The first applications where proving the correctness of cache coherence protocols for multiprocessors, networking protocols for telecommunications, and then verifying floating point arithmetic, a problem motivated by the famous FDIV bug of the Intel Pentium® processor. Formal verification tools are now a standard part of the design of large, VLSI chips.

More recently, advances in SAT solving techniques have brought formal verification into use in software development. SAT (boolean satisfiability) is the “canonical” NP-complete problem. Nevertheless, practical solving techniques have been developed that allow problems with thousands to tens of thousands of variables to be solved. SMT solvers extend SAT by including decision procedures for non-boolean problems such as linear inequalities, polynomial inequalities, or simple data structures and arrays. With such techniques, researchers are developing tools to search for many classes of errors including usage errors of synchronization primitives (e.g. failing to release a lock), buffer overflows, failure of device driver calls to terminate, etc. These techniques are being employed in industry, and the field is advancing rapidly.

This course explores the underlying algorithms and methods of formal verification including satisfiability checking of propositional formulas and model checking. We look at methods for specification, modeling, and abstraction. Real-world examples from industry and promising examples from current research are presented throughout the course.

## Specifics

• Lectures: Tuesday/Thursday, Dempster 101, 11:00am-12:30pm
• First lecture: September 10.
• Instructor: Mark Greenstreet
• Course name: The "official" name of this course (i.e. in the UBC calendar) is "Integrated System Design."
The name is obsolete. This course is an introduction to formal verification. The course remains "integrated" in the sense that it covers the theory and practice of formal verification with applications from hardware, software, and cyber-physical systems.
• Textbook: none. There will be papers from the research literature. See the reading list for more details.
• Homework: I intend to have four assignments where you will try examples with different tools such as a BDD (symbolic boolean) package, Z3 (a state-of-the-art SMT solver), and other tools. The homework assignments (and maybe solutions) will be posted here.
• Project: I'll define the details as the course continues. The goal of your project is to produce a master's thesis proposal. To get more details, click here. I'll post some project ideas within the first week of the term.
• Source Code: Source code, documentation, jar files, etc. for the jython BDD package for this class is available here. If we use other software packages as the term goes on, I'll link them to the same page.
• See also: I used Alan Hu's version of the course as my starting point for the topics and papers. Click here to see the web-page for this course.