Keynote Presentation - John Launchbury
Presented as part of the 2017 HCSS conference.
Abstract:
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.
__
Dr. John Launchbury joined DARPA as a Program Manager in July 2014 and was named Director of the Information Innovation Office (I2O) in September 2015. In this role he develops Office strategy, staffs the Office, and works with I2O program managers to develop new programs and transition program products. Dr. Launchbury has been instrumental in formulating and implementing I2O research thrusts in programming languages, security, privacy and cryptography.
Before joining DARPA, Dr. Launchbury was 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. Under his leadership, the company experienced strong growth, successfully delivered on multiple contract awards and was recognized for thought leadership in high-assurance technology development.
Prior to founding Galois, Dr. Launchbury 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, the Haskell programming language in particular.
Dr. Launchbury received first-class honors in mathematics from Oxford University in 1985, holds a Ph.D. in computing science from the University of Glasgow and won the British Computer Society's distinguished dissertation prize. In 2010, Dr. Launchbury was inducted as a Fellow of the Association for Computing Machinery (ACM).