|
|
Progress on the Verified Software Grand Challenge
Dr. Bruce W. Weide
Thursday, March 27, 2008
10:30AM ~ 11:30AM, Harris Center 101
Abstract
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.
Short Bio
Bruce W. Weide is Professor 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.
|
|
