Verified Approximate Computing

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 change the semantics of an application to enable it to navigate this trade-off space and meet its performance requirements. Examples of these mechanisms include skipping portions of the application's computation and running the application on fast unreliable hardware systems for which operations may silently produce incorrect results with some non-negligible probability.

I present a program verification and analysis system, Rely, for answering fundamental questions that arise when changing the semantics of an application to produce an approximate application. For example, 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 application.
Michael Carbin is a Ph.D. Candidate in Electrical Engineering and Computer Science at MIT. Michael started his research career as undergraduate student, working on BDD-based program analysis at Stanford University and on type-safe compile-time metaprogramming at Microsoft Research. His work at Stanford received an award for Best Computer Science Undergraduate Honors Thesis.

As a graduate student, Michael has worked as a MIT Lemelson Presidential Fellow and a Microsoft Research Graduate Fellow on both the theory and practice of verified approximate computing and software self-healing. His recent research on verifying the reliability of programs that execute on unreliable hardware won a best paper award at OOPSLA 2013: Object-Oriented Programming, Systems, Languages & Analysis.