Santosh NagarakatteAnother cool result from my research group that I am excited about upcoming at ARITH 2026: "Odd but Error-Free FastTwoSum". See the preprint here:
https://arxiv.org/pdf/2601.17198
Great work by my PhD student Sehyeok Park and collaborator Jay Lim.
A new piece of research as part of my group's safe and formally verified numerics project that I am really excited about -- The FLoPS framework, which formalizes the upcoming P3109 standard in Lean. Great work by my PhD students: Tung-Che Chang and Sehyeok Park and collaborator Jay Lim from University of California, Riverside.
The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike the fixed types of IEEE-754, P3109 introduces a parametric framework defined by bitwidth, precision, signedness, and domain. This flexibility results in a vast combinatorial space of formats -- some with as little as one bit of precision -- alongside novel features such as stochastic rounding and saturation arithmetic.
We have formalized the P3109 standard and discovered new interesting properties of foundational algorithms such as Fast2Sum, Sternbenz, and a floating-point splitting ExtractScalar in the context of P3109.
During this process, we discovered some errors in the draft standard and reported it to the working group (I am member of the P3109 working group). They have been fixed.
See the Github repo of our mechanized proofs in Lean: https://github.com/rutgers-apl/flops
See our technical report:
https://arxiv.org/pdf/2602.15965
On a side note, I was convincingly persuaded to explore Lean by Ilya Sergey when I visited NUS in August 2024. Thanks Ilya for making a compelling case for using Lean while Umang Mathur and Abhik Roychoudhury made the visit possible.
I gave a talk on our work on verifying the eBPF verifier in the Linux kernel at the Linux Storage, Filesystem, Memory Management & BPF Summit, March 2025, Montreal, Canada. Daroc Alden from Linux Weekly News has written a nice summary article on the talk. Here is the link: https://lwn.net/Articles/1020664/
#Rutgers #RutgersCS
#Rutgers #RutgersCS
Just learned that the Rutgers Board of Governors has approved my promotion to Full Professor with tenure effective July 1st. Thanks to all my current and graduated PhD students, mentors, and the broad PL/Arch/Verification community. Here is a group photo of my 6 graduated PhD students. #rutgers #rutgerscs
Our paper "Verifying the verifier: eBPF Range Analysis Verification" accepted at CAV 2023. Work with students Hari and Matan, and colleague Srinivas Narayana. We propose an automated method to check the correctness of range analysis in the Linux Kernel’s eBPF verifier.
We automatically generate verification conditions that encode the operation of eBPF verifier directly from Linux Kernel’s C source code and check it against our specification.
When we discover instances where the eBPF verifier is unsound, we propose a method to generate an eBPF program that demonstrates the mismatch between the abstract and the concrete semantics.
We automatically check the soundness of the eBPF verifier for 16 versions of the eBPF verifier in the Linux Kernel ranging from 4.14 to 5.19. In this process, we have discovered new bugs in older versions and proved the soundness of range analysis in the latest kernel. Here is the link to the preprint: https://people.cs.rutgers.edu/~sn349/papers/agni-cav2023.pdf
Here is a talk summarizing our RLIBM project, where we are building correctly rounded math libraries. https://www.youtube.com/watch?v=vAcf6d26kiM #RLIBM #RutgersCS
