2014 Bower Science Award Theme: Verification of Computer Systems
A major challenge of modern computer technology and digital electronics is that they have surpassed the limits of human perception. When a digital electronic device malfunctions, such as a microprocessor controlling the ailerons of a passenger jet, or an MRI machine being used for a critical medical diagnosis, human lives are at stake. But one can't simply open up a panel and glance inside like popping the hood of a car. All of the important action in a computer takes place on the subatomic level, imperceptible to human senses. How, then, are humans to find and identify when something goes wrong in the complex, near-light-speed processes of hardware and software? Or to confirm that a new hardware design or software package will do everything it is supposed to do?
Answering those questions is the realm of model checking, a field of computer science that was pioneered and fully defined by mathematician Edmund Clarke. Model checking bypasses the laborious manual and step-by-step verification and testing of a hardware or software model, which is still subject to human error, by considering a computer system on a broader level—namely, as a mathematical object that behaves subject to certain principles that can be logically defined and determined in a completely automated process. Clarke first set out the principles and techniques of model checking for finite-state systems in a seminal 1981 paper published with his graduate student, E. Allen Emerson. That paper launched a flood of further research and development of model checking theory and applications, much of it led by Clarke and those who had studied under him.
Mathematical theories and techniques may be elegant and beautiful, but that doesn't mean they are necessarily practical or useful in the real world. Clarke's work, however, proved its value almost immediately, with his techniques adopted by major hardware manufacturers such as IBM, Motorola, Texas Instruments, Intel, and Apple. It is probably safe to say that nearly all microprocessor chips and other integrated circuits are verified and checked for bugs with Clarke's model checking methods.
After completing his undergraduate work in mathematics at the University of Virginia, Clarke moved on to Duke University for his master's degree. He earned his Ph.D. from Cornell in computer science in 1976. He taught at Duke and Harvard before joining the faculty at Carnegie Mellon in 1982. Now FORE Systems University Professor Computer Science at Columbia, Clarke has published nearly 400 papers and other works, including his influential textbook Model Checking, considered a standard in the field.
Edmund Clarke continues to bridge the gaps between mathematical abstraction and practical applications through the development and expansion of model checking and verification. While we may never be able to fully escape computer bugs in our ever more complex hardware and software, Clarke's work is our strongest bulwark against them.and thus a major factor in the creation of faster, more powerful, and more reliable computer systems.
Information as of April 2014