February 21, 2008 - Bruce Weide

Title: Progress on the Verified Software Grand Challenge

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.