<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><h1 class="page__title title" id="page-title">Verified Approximate Computing</h1><div><span name="x"></span><span class="event-speaker">
<a href="http://people.csail.mit.edu/mcarbin/">Michael Carbin</a>, </span><span class="event-speaker-from"><a href="http://web.mit.edu/">Massachusetts Institute of Technology</a><br>Monday, March 24, 4:30pm<br>Computer Science 105<br></span><br><span class="event-speaker-from">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.<br><br>
</span><p>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?</p>
<p>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.</p><p><br></p>
<p>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. <br></p><span class="event-speaker-from"><br>
</span></div><br><br></div></body></html>