Somewhat ironically, just as traditional systems software finally comes within reach of detailed mathematical verification, the demand for verification technology is rapidly expanding into domains that pose very different kinds of challenges. How could a face recognition technology be verified, for example, when it is not clear even how to state a correctness property? Or how should we attempt to verify an autonomous system like a self-driving car? This talk will attempt to lay out the problem space, and offer some ideas for how the verification community might start tackling the problem of assuring AI.

Speaker bio

John Launchbury is Chief Scientist of Galois, Inc., which he founded in 1999 to address challenges in information assurance through the application of functional programming and formal methods. He has recently returned to Galois after a three-year stint at DARPA, where he served as a Program Manager and then Director of the Information Innovation Office. Prior to founding Galois, John was a full professor in Computer Science and Engineering at the Oregon Graduate Institute (OGI) School of Science and Engineering, which was subsequently incorporated into the Oregon Health and Science University. At OGI, he earned several awards for outstanding teaching and gained international recognition for his work on the analysis and semantics of programming languages, Haskell in particular. John holds a Ph.D. in computing science from the University of Glasgow and won the British Computer Society’s distinguished dissertation prize. In 2010 he was inducted as a Fellow of the Association for Computing Machinery (ACM).