Making proof-based verified computation almost practical
I will describe a project at UT Austin that challenges the second piece of this folklore. We have developed an interactive protocol that begins with an efficient argument [IKO CCC '07] and incorporates new theoretical work to improve performance by 20+ orders of magnitude. In addition, we have broadened the computational model from Boolean circuits to a general-purpose model. We have fully implemented the system, accelerated it with GPUs, and developed a compiler that transforms computations expressed in a high-level language to executables that implement the protocol entities.
The resulting system, while not quite ready for the big leagues, is close enough to practicality to suggest that in the near future, PCPs could be a real tool for building actual systems.
Talk will be based on these papers and ongoing work:
Michael Walfish is an assistant professor in the Computer Science Department at The University of Texas at Austin. His research interests are in systems, security, and networking. His honors include an Air Force Young Investigator Award, an NSF CAREER Award, a Sloan Research Fellowship, a Teaching Excellence Award from the UT College of Natural Sciences, the Intel Early Career Faculty Honor Program, and the UT Society for Teaching Excellence. He received his B.A. from Harvard and his Ph.D. from MIT, both in Computer Science.