Monday, October 14, 2019 - 4:00pm to 4:50pm
Gilfillan Auditorium

Speaker Information

Bill Harris
Principal Scientist
Galois Inc.

Abstract

The grand challenge of program verification and synthesis is to enable programmers to write programs and have assurance that the result is correct. Work since the foundation of the field has aimed to solve this challenge. Yet in practice, programmers are left to tackle critical programming problems with inadequate support from programming tools. In particular,


1. Companies continuously run wasteful sets of database queries with enormous computational costs, in part because they do not have automated methods for identifying redundant queries;

2. Parsers for practical data formats are often developed manually (and as a result, inevitably contain errors), in part because foundational approaches for synthesizing parsers cannot capture the critical features of actual formats in use;

3. Secure computations between mutually-distrusting parties can only be implemented by a small handful of cryptography experts, in part because of the mismatch between program representations directly supported by cryptographic protocols and the language constructs needed to implement practical tasks.

In this talk, I will present recent and planned work that I am performing with colleagues at Galois Inc. and an array of academic institutions that aims to address these problems. Taken broadly, our work illustrates the unique challenges that arise when making program verification work in practice.

Speaker Bio

Bill Harris is a Principal Scientist at Galois Inc.; his work broadly aims to extend and apply techniques from program verification and synthesis to enable the development of correct and secure programs. In 2014, he received his PhD in Computer Science from the University of Wisconsin-Madison, where he was advised by Somesh Jha and Tom Reps; he has also served on the faculty at the Georgia Institute of Technology. He was supported by a Microsoft PhD Fellowship from 2010 to 2011.