A “verifying compiler” (a tool that, in its purest form, would compile only programs that it could prove correct) has long been a dream of the software formal methods community. Jim King apparently coined the term in his 1969 Ph.D. thesis, and 35 years later Tony Hoare proposed the development of a verifying compiler as a “Grand Challenge for Computing Research”. What have we been doing all this time?!? Visions of verification foundations and technology that would qualify as meeting Hoare’s challenge have driven the research of the OSU Reusable Software Research Group for two decades. In this talk, I will try to explain how a verifying compiler might work, why it would be a significant advance over current practice, why it is still considered a “challenge”, and why there is hope that a verifying compiler (hence, verified software) is truly feasible.
Speaker Biography
Bruce W. Weide is Professor and Associate Chair of Computer Science and Engineering at The Ohio State University, where he co-directs the Reusable Software Research Group with Bill Ogden. His research interests include all aspects of software component engineering, especially in applying RSRG work to practice and in teaching its principles to beginning CS students. He and colleague Tim Long were awarded the IEEE Computer Society’s 2000 Computer Science and Engineering Undergraduate Teaching Award for their work in the latter area. Weide holds a Ph.D. in Computer Science from Carnegie Mellon University and a B.S.E.E. from the University of Toledo. He is a member of the IEEE, ACM, and UCS.