The Department of Computer Sciences is proud to announce the annual Visions of Computer Sciences Research Lectures. The first lecture will be held Friday, January 25, 2002. Formal Methods is the topic this year.
Lectures: 4:00 - 5:00 p.m. Avaya Auditorium, ACES 2.302
Reception: 5:00 - 6:00 p.m. Faculty Lounge, ACES 6.102
The Case Against a Grand Unification Theory
Great challenges exist in developing and teaching the principles of software design. General theories for software design are too weak to be of value to the practitioners. Specialized theories that are developed for specific domains should play a central role, along with the structuring principles that bind the theories together.
Jayadev Misra - Schlumberger Chair in Computer Sciences
Jayadev Misra is a Professor in Computer Sciences at The University of Texas at Austin. His research interests are in distributed computing and foundations of programming theory. His primary focus at present is applying formal methods in practice, particularly in the specifications and designs of synchronous and asynchronous systems. Dr. Misra is a Fellow of the IEEE and ACM. He was a Guggenheim Fellow during 1989.
Models: Moore and More
As computers become ubiquitous, methods for ensuring correct program behavior become increasingly important. Classic manual proof-theoretic techniques have been studied for three decades, but due to the extraordinary mathematical demands placed on programmers, their practical applicability is hindered. For two decades, I have been developing an alternative, automated model-theoretic approach to program reasoning. One manifestation is model checking, a fully algorithmic method for checking that a finite model of program meets a temporal logic specification. An obvious criticism is the state explosion problem. Surprisingly, this has turned out to be much less severe in practice than expected. In this talk, I will discuss why. I will also explain my belief that advances in abstraction together with Moore's law mean that the effectiveness of model-theoretic methods will continue to scale up in the future.
E. Allen Emerson - Endowed Professor in Computer Sciences
E. Allen Emerson's research interests center around formal methods for establishing program correctness. He is co-recipient of the ACM Kanellakis Theory and Practice Award for the invention of symbolic model checking, a method for establishing correctness of computer systems widely used in the computer hardware industry and showing promise for software. He also serves as an editor for leading formal methods journals including ACM Transactions on Computational Logic, Formal Aspects of Computing, and Formal Methods in Systems Design.
The Visions poster for January 25th may be downloaded in PDF format.