[Colloquium] Computer Science Seminar - February 10, 2014

[Sandra Wallace]

Michael Carbin
Massachusetts Institute of Technology (MIT)

Date:  Monday, February 10, 2014

Time:  2:30 PM

Place: Ryerson 251
 
Title:	  “Verified Approximate Computing”
 
Abstract: 
Many modern applications implement large-scale computations (e.g., machine learning, big data analytics, and financial analysis) in which there is a natural trade-off between the quality of the results that the computation produces and the performance and cost of executing the computation.  Exploiting this fact, researchers have recently developed a variety of new mechanisms that automatically manipulate an application to enable it to execute at a variety of points in its underlying trade-off space. The resulting approximate application can navigate this trade-off space to meet its performance and cost requirements.

I present a program verification and analysis system, Rely, for answering fundamental questions that arise when manipulating an application that implements an approximate computation. Examples of the questions that Rely is designed to answer include: What is the probability that the approximate application produces the same result as the original application? How much do the approximate application’s results differ from those of the original application? And is the approximate application safe and secure?

Rely answers these questions with a novel analysis and verification method for reasoning about the safety and accuracy of approximate applications. Rely also provides a novel language and program analysis for verifying quantitative reliability: the probability that the new approximate application produces the same result as the original computation.is problem reduced it to O(r) bits [Kotlov-Lovasz'96, Kotlov '97] and more recently to O(r/log(r)) bits assuming a number theoretic conjecture [BenSasson-L-RonZewi'12]. In this work, we prove an (unconditional) upper bound of O(r^{1/2} log®) bits.
 
Host:  Hank Hoffmann
 
*Refreshments will be served after the talk at 3:30 pm in Ryerson 255*



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20140204/b0b03af2/attachment.htm