Monday Keynote, 16. November, 14:00 - 15:00

Formal Methods: From Start to Limit

E. Allen Emerson, University of Texas

Abstract

Computer systems exhibit complex and unanticipated behavior. The notion that it might be necessary to mathematically prove that a computer program exhibits the desired behavior can be traced back at least as far as Turing. Today, model checking, a technique based on state space search rather than proof, has shown itself surprisingly useful in routinely performing a range of verification tasks, in particular for hardware verification. The utility of model checking has hinged on the ability to express correctness properties of interest, and the amelioration of state explosion. Even with advances in abstraction and compact symbolic representation, however, there is still a gulf in size between the verifiable systems and numerous practical systems that still exhibit unpredictable behavior. Moreover, the very formality of assertion languages for expressing correctness limits their intuitive understandability, and discourages their broader adoption beyond a band of formal methods experts. The disparity in notation describing the system implementation versus the specification formalism is another complication.

Placed in a larger context, we would argue that the central problem, which is by no means solved, is how to program: how to develop a program (meaning, e.g., software program, hardware design, or embedded system) that exhibits the intended behavior. In this talk we address several aspects of this issue ranging from standard but important verification fare such as improved efficiency. more convenient specification, and the need for more workable divide-and-conquer reasoning to more ambitious strategies such as program synthesis and repair.

Bio

E. Allen Emerson is co-recipient of the 2007 ACM A.M. Turing Award for the invention and development of model checking. His other scientific interests include automata, dynamical systems, and automated program synthesis. He received the BS in Mathematics from the University of Texas, and the PhD in Applied Mathematics from Harvard University. He is now Regents Chair and Professor of Computer Science at the University of Texas.