Zach Tatlock is an Assistant Professor in Computer Science and Engineering at the University of Washington where he is a member of the Programming Languages and Software Engineering (PLSE) group. He received his PhD from UC San Diego and BS from Purdue. His research draws upon proof assistants, SMT solvers, and type systems to improve software reliability and security in domains ranging from distributed systems and compilers to web browsers. He can juggle and solve Rubik's cubes, but not at the same time.
Talk InformationAutomatically Improving Accuracy for Floating Point Expressions10:00 AM February 3, 20172250 WEB
Most engineering and scientific computer programs follow mathematical models described by real numbers, but use floating point arithmetic internally. Sometimes the two number systems give rather different results, and when that happens programmers are often ill-equipped to improve the accuracy of their code. Experts in numerical methods can fix these problems by rearranging computations, but acquiring that expertise can take years. My colleagues and I are working to bridge this gap with Herbie, a tool that automatically improves the accuracy of floating point expressions.
In this talk I will describe the techniques Herbie uses to automatically improve floating point accuracy using a guided, heuristic search. Herbie applies algebraic rewrites and series expansions to generate potentially-more-accurate versions of the program, then samples inputs to evaluate, prune, and combine these candidates into a new, more-accurate program. We've used Herbie on expressions found everywhere from textbooks to large-scale surveys of open-source software, and consistently find good results. I'll also briefly discuss next steps for Herbie: scaling up to larger codebases and a new format to standardize floating point benchmarks.