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.
The rapidly emerging developments in AI, Machine Learning, and Robotics bring new challenges: will the robot do the right thing? How do we reason about cyber-physical systems operating in physical space and time? Can we show that a learning algorithm will produce solutions that always satisify critical requirements? Can we apply these methods to further automate verification algorithms?
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.