My research aims to build floating-point analysis tools for programs as developers write them, and to make these tools accessible to developers. To get there, I focus on three questions:

How can we verify the floating-point features developers actually use? Most floating-point verification tools target small numerical kernels or specialized languages. Instead, I am actively integrating floating-point verification techniques into a deductive verifier for a general-purpose language, Stainless for Scala. Guided by our large-scale study of how developers use floating-point in practice (OOPSLA '26), we added bit-precise floating-point reasoning to Stainless (TACAS '26), and I am now working on a scalable roundoff error analysis for branching programs, where the real-valued and floating-point executions can take different paths.

How do we know floating-point analysis tools work on real-world code? Verification tools are mostly evaluated on small, hand-picked examples, which says little about how they perform on real-world code. We mined GitHub for floating-point code and extracted a dataset of 10 million floating-point functions (OOPSLA '26). We used this dataset to build benchmarks for evaluating our integration of bit-precise floating-point reasoning into Stainless (TACAS'26) and our ongoing work on roundoff analysis of branching programs. A BSc thesis I supervised extends this approach to automatically extract benchmarks from Rust code.

How can developers actually use these tools? Deductive verifiers can provide strong guarantees but remain hard to use for non-experts. I am studying where users struggle and how tools can better support them, through a supervised MSc thesis and an ongoing follow-up project, and I plan to extend this to floating-point analysis tools.