Eva is an associate professor at the Dept. of Information Technology at Uppsala University, and adjunct faculty at MPI-SWS. Previously, she was a tenure-track faculty at MPI-SWS, and before that, she did her PhD with Viktor Kuncak at EPFL. She is generally interested in programming languages, software verification, program synthesis and approximate computing.
Floating-point arithmetic enables efficient numerical computations, but is also notorious for being unintuitive due to its special values as well as rounding operations, the latter inevitably introducing errors at most arithmetic operations. One way of making sure that computed results are meaningful, i.e. accurate enough, even in the presence of such errors is to use a static analyzer that bounds the worst-case rounding errors.
In this talk, I will give an overview of our recent research results and tools on formal verification of floating-point programs, focusing in particular on what is possible today when analyzing functional programs.