Zachary Tatlock
Assistant Professor, Computer Science and Engineering, University of Washington


Bio

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 Information

  • Automatically Improving Accuracy for Floating Point Expressions
  • 10:00 AM February 3, 2017
  • 2250 WEB

  • Abstract
    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.

    Schedule

    TimePlanAppointmentLocation
    2017-02-03 10:00:31Talk-2250 WEB
    2017-02-03 13:00:50FP StuffGanesh, Zvon?MEB 3436
    2017-02-03 13:30:00Floating-points and stuffZvonimir RakamaricMEB 3424
    2017-02-03 14:00:00catch on on awesome compiler stuff; I'm flexiJohn RegehrMEB 3470
    2017-02-03 14:30:00Ganesh 1-1ganesh@cs.utah.edu3428 MEB
    2017-02-03 15:00:001-1Jarkko SavelaMEB 3436
    2017-02-03 15:30:001-1Mohammed S. Al-MahfoudhMEB 3436
    2017-02-03 16:00:00stuffEric Eide3476 MEB
    2017-02-03 16:30:00Verdi, and runtime verification of distributeMaryamMEB 3157

    Sign Up

    Add Homepage Link?