Keynote Speech I
Verification Tools Should Certify Their Results
Randal E. Bryant
Carnegie Mellon University
Abstract
Verification tools check that a system meets a specified set of properties. For example, a verifier may check whether two digital circuits have identical functionality or that a software device driver adheres to a set of interface requirements. Such tools have become critical components in the design and validation of both hardware and software.
One shortcoming of these tools is that bugs in their algorithms or their implementations may cause them to produce incorrect results. They may even state that the verification conditions are satisfied, even though the system being verified contains some critical flaw. Indeed, internal bugs are inevitable, given the complexity of these tools and the extensive engineering to maximize their performance. This is particularly vexing for formal verification tools, where they claim to provide rigorous results.
The reliability of a verification tool can be greatly improved by requiring it to be self certifying, generating a certificate demonstrating that the provided answer is correct. This has become a common capability for Boolean satisfiability (SAT) solvers. When they determine that the formula is satisfiable, they generate a satisfying solution. For an unsatisfiable formula, they generate a checkable proof that the formula is indeed unsatisfiable. This proof can be checked by a simple program that itself has been formally verified. Such a capability means that the answers provided by the tool can be fully trusted, even if the tool itself is buggy.
This talk describes recent work on certifying the results from a variety of tools, including SAT solvers, SMT solvers, knowledge compilers, and model checkers. These capabilities provide not only valuable assurances to the end users, they also help developers create more reliable tools.
Biography
Randal E. Bryant is Founder's University Professor of Computer Science Emeritus at Carnegie Mellon University. He has Carnegie Mellon University since 1984, starting as Assistant Professor. He served as Dean of the School of Computer Science from 2004 to 2014.
Dr. Bryant's research focusses on methods for verifying the correctness of digital hardware and software. He is best known for the development of Ordered Binary Decision Diagrams (OBDDs), a data structure for representing and reasoning about digital functions. His research has been widely used by semiconductor companies worldwide. He has received awards from leading professional societies and industry associations. He is a member of the U.S. National Academy of Engineering.
Dr. Bryant has taught courses across a variety of topics in computer science and computer engineering. Along with David R. O'Hallaron, he developed a novel approach to teaching about the hardware, networking, and system software that comprise a system from the perspective of an advanced programmer, rather than from those of the system designers. Their textbook ``Computer Systems: A Programmer's Perspective,'' now in its third edition, is in use at over 375 institutions worldwide, with translations into five languages.
Dr. Bryant spent the 1989-1990 academic year as a Visiting Research Fellow at Fujitsu Laboratories in Kawasaki, Japan. He spent the 2014-2015 academic year as Assistant Director for Information Technology Research and Development at the White House Office of Science and Technology Policy (OSTP).
Dr. Bryant received his B.S. in Applied Mathematics from the University of Michigan in 1973, and his PhD in computer science from MIT in 1981. He was an assistant professor at Caltech from 1981 to 1984.