Formalized Skia’s 2D rasterization semantics in Lean and built a verified optimizer that achieves an average speedup of 18.7% across the top 100 websites by traffic.
Mixing Condition Numbers and Oracles for Accurate Floating-point Debugging
IEEE ARITH’25
Bhargav Kulkarni, Pavel Panchekha
Built a floating-point debugger combining double-double arithmetic, condition numbers, and logarithmic oracles, achieving 80.0% precision and 96.1% recall on 546 difficult numeric benchmarks.
Employment
Adobe Inc.
2026
Graduate Research Intern
Building an optimizer for scene-graphs in Adobe Photoshop
University of Utah
2023—Present
Research Assistant
Currently building a verified optimizer for the Skia vector graphics engine that powers Chrome rendering.
Formalized Skia’s semantics in the Lean theorem prover to verify optimizing rewrites.
Previously adapted floating-point static analysis techniques to build an accurate floating-point debugger.
NASA Langley Formal Methods Group
2024
Research Intern
Worked on generating proof certificates for the PVS automated theorem prover to verify Herbie’s (a floating-point superoptimizer) accuracy-aware optimizations
Skills and Projects
General Programming: Python, Racket, Java
Systems Programming: C/C++, Bash, Rust
Hardware: Verilog, x86
Trinity Game Engine: A game engine and byte code VM for scripting. [source]
Logic in Coq: Classical propositional logic and natural deduction in Coq/Rocq. [source]
CheemScheme: Scheme dialect in C++ with tail recursion and error reporting. [source]