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.