About

Professor Santosh Nagarakatte leads the Rutgers Architecture and Programming Languages (RAPL) Research Group at the Department of Computer Science, Rutgers University. His research focuses on developing techniques to build robust and secure computer systems through program analysis and lightweight formal methods. The group actively works on projects related to verifying and improving the soundness of system components such as the eBPF verifier in the Linux kernel, as well as creating high-performance, correctly rounded mathematical libraries for floating point and posit number representations. Professor Nagarakatte's work has been recognized with multiple awards and research grants from organizations including the National Science Foundation, Intel Corporation, and the eBPF Foundation. His research contributions span formal verification, compiler optimizations, numerical methods, and hardware-software co-design, with a strong emphasis on practical tools and methods that enhance system reliability and security.

Research topics

• Computer Science
• Artificial Intelligence
• Mathematics
• Algorithm
• Embedded system
• Operating system
• Arithmetic
• Information Retrieval
• Programming language
• Parallel computing
• Database
• Machine Learning
• Computer hardware
• Computer engineering
• Distributed computing
• Pure mathematics
• Computational science
• Discrete mathematics
• Theoretical computer science

Selected publications

• FLoPS: Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean

  ArXiv.org · 2026-02-17

  articleOpen accessSenior author

  The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike 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. These deviations create a unique verification gap that this paper intends to address. This paper presents FLoPS, Formalization in Lean of the P3109 Standard, which is a comprehensive formal model of P3109 in Lean. Our work serves as a rigorous, machine-checked specification that facilitates deep analysis of the standard. We demonstrate the model's utility by verifying foundational properties and analyzing key algorithms within the P3109 context. Specifically, we reveal that FastTwoSum exhibits a novel property of computing exact "overflow error" under saturation using any rounding mode, whereas previously established properties of the ExtractScalar algorithm fail for formats with one bit of precision. This work provides a verified foundation for reasoning about P3109 and enables formal verification of future numerical software. Our Lean development is open source and publicly available.

  PublisherOA PDF

• Odd but Error-Free FastTwoSum: More General Conditions for FastTwoSum as an Error-Free Transformation for Faithful Rounding Modes

  Open MIND · 2026-01-23

  preprintSenior author

  This paper proposes sufficient, yet more general conditions for applying FastTwoSum as an error-free transformation (EFT) under all faithful rounding modes. Additionally, it also identifies guarantees tailored to round-to-odd for establishing FastTwoSum as an EFT. This paper also describes a floating-point splitting tailored for round-to-odd that is an EFT where the distribution of bits is configurable (i.e., ExtractScalar for round-to-odd). Our sufficient conditions are more general than those previously known in the literature (i.e., it applies to a wider operand domain).

  DOI

• Odd but Error-Free FastTwoSum: More General Conditions for FastTwoSum as an Error-Free Transformation for Faithful Rounding Modes

  ArXiv.org · 2026-01-23

  articleOpen accessSenior author

  This paper proposes sufficient, yet more general conditions for applying FastTwoSum as an error-free transformation (EFT) under all faithful rounding modes. Additionally, it also identifies guarantees tailored to round-to-odd for establishing FastTwoSum as an EFT. This paper also describes a floating-point splitting tailored for round-to-odd that is an EFT where the distribution of bits is configurable (i.e., ExtractScalar for round-to-odd). Our sufficient conditions are more general than those previously known in the literature (i.e., it applies to a wider operand domain).

  PublisherOA PDF

• FLoPS: Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean

  Open MIND · 2026-02-17

  preprintSenior author

  The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike 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. These deviations create a unique verification gap that this paper intends to address. This paper presents FLoPS, Formalization in Lean of the P3109 Standard, which is a comprehensive formal model of P3109 in Lean. Our work serves as a rigorous, machine-checked specification that facilitates deep analysis of the standard. We demonstrate the model's utility by verifying foundational properties and analyzing key algorithms within the P3109 context. Specifically, we reveal that FastTwoSum exhibits a novel property of computing exact "overflow error" under saturation using any rounding mode, whereas previously established properties of the ExtractScalar algorithm fail for formats with one bit of precision. This work provides a verified foundation for reasoning about P3109 and enables formal verification of future numerical software. Our Lean development is open source and publicly available.

  DOI

• Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode

  Proceedings of the ACM on Programming Languages · 2025-06-10 · 1 citations

  articleOpen accessSenior author

  Our RLibm project has recently proposed methods to generate a single implementation for an elementary function that produces correctly rounded results for multiple rounding modes and representations with up to 32-bits. They are appealing for developing fast reference libraries without double rounding issues. The key insight is to build polynomial approximations that produce the correctly rounded result for a representation with two additional bits when compared to the largest target representation and with the "non-standard" round-to-odd rounding mode, which makes double rounding the RLibm math library result to any smaller target representation innocuous. The resulting approximations generated by the RLibm approach are implemented with machine supported floating-point operations with the round-to-nearest rounding mode. When an application uses a rounding mode other than the round-to-nearest mode, the RLibm math library saves the application's rounding mode, changes the system's rounding mode to round-to-nearest, computes the correctly rounded result, and restores the application’s rounding mode. This frequent change of rounding modes has a performance cost. This paper proposes two new methods, which we call rounding-invariant outputs and rounding-invariant input bounds, to avoid the frequent changes to the rounding mode and the dependence on the round-to-nearest mode. First, our new rounding-invariant outputs method proposes using the round-to-zero rounding mode to implement RLibm's polynomial approximations. We propose fast, error-free transformations to emulate a round-to-zero result from any standard rounding mode without changing the rounding mode. Second, our rounding-invariant input bounds method factors any rounding error due to different rounding modes using interval bounds in the RLibm pipeline. Both methods make a different set of trade-offs and improve the performance of resulting libraries by more than 2X.

  PublisherDOI

• Automatic Synthesis of Abstract Operators for eBPF

  2025-08-19

  articleOpen accessSenior author

  This paper proposes an approach to automatically synthesize sound and precise abstract operators for the static analyzer in the eBPF verifier. The eBPF verifier ensures that only safe user-defined programs are loaded into the kernel. An unsound operator can lead to unsafe programs being accepted, while an imprecise operator can cause safe programs to be rejected. Our approach starts by generating candidate operators using input-output examples tailored for the eBPF verifier's abstract operators and iteratively refines it for soundness and precision. Using this approach, we have generated more precise variants of existing operators. Our approach also generates numerous sound and unsound operators that can serve as test suites for existing eBPF verification and fuzzing frameworks.

  PublisherDOI

• Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel

  Lecture notes in computer science · 2025-01-01 · 2 citations

  book-chapterSenior author
  PublisherDOI

• Assessing the knowledge of students regarding post matric scholarship scheme

  International Journal of Agriculture Extension and Social Development · 2025-06-01

  articleOpen access1st authorCorresponding

  This study aimed to Assessing the knowledge of students regarding post matric scholarship scheme. A random sampling approach was utilized to select 240 undergraduate students from two universities: Chaudhary Charan Singh Haryana Agricultural University and Guru Jambheshwar University of Science and Technology, Hisar. To gather data, an interview schedule was designed and implemented. The findings revealed that all respondents from both Chaudhary Charan Singh Haryana Agricultural University (CCS HAU) and Guru Jambheshwar University of Science and Technology (GJUS&T) were aware that both male and female students were eligible to apply for the post-matric scholarship, and that the application process followed a hybrid model. However, awareness of the scholarship's governing body was notably low, with only a small fraction of respondents recognizing that the Ministry of Social Justice and Empowerment administered the program, 5.83 per cent from CCS HAU and 2.50 per cent from GJUS&T, respectively. It was found that all respondents from both institutions were aware of the eligibility criteria for post-matric scholarships. These criteria included securing at least 50% marks in the previous examination, holding Indian citizenship, belonging to the SC, BC, or EWS categories, and having a family income below ?2.5 lakh per annum. Additionally, students knew that applications could be submitted through the Common Service Centre (CSC).

  PublisherOA PDFDOI

• Comparing the Precision of Abstract Operators in the eBPF Verifier Using Differential Synthesis

  Lecture notes in computer science · 2025-10-06

  book-chapterSenior author
  PublisherDOI

• Influence of growing media and nutrient levels on growth and yield of lettuce (Lactuca sativa L.) in hydroponics

  Crop Research · 2025-07-05

  article

  Hydroponics has become one of the most popular approaches in modern agricultural production, offering efficient and sustainable crop cultivation. Growing media play a vital role in its success by influencing nutrient availability, water retention, and root development. Understanding their interaction with nutrient levels is crucial to maximizing crop performance under hydroponic systems. This study was conducted at the Hi-Tech Hydroponics Unit, M. S. Swaminathan School of Agriculture, Centurion University of Technology and Management, Odisha, India, during the winter season (October to December), 2024. The study aimed to investigate the impact of growing media and varied nutrient levels on lettuce in hydroponic systems by using Factorial CRD. Growing media consisting of coco coir, oasis cubes, rockwool, and potting mix were used in the present study. Plants were grown using the nutrient film technique (NFT) structure with varied concentrations of Hoagland solution (600 ppm, 800 ppm, 1000 ppm, and 1200 ppm). The Lollo Rosso lettuce was used as a test crop. Data were recorded on plant parameters such as number of leaves, plant height, leaf fresh weight, and yield on a fresh weight basis. Among the nutrient levels, 1200 ppm was the most effective in enhancing the growth attributes of lettuce at harvest, viz., number of leaves (12.5), plant height (16.6 cm), leaf fresh weight (7.4 g/leaf), and yield (93 g/plant). Amongst growing media, the potting mix resulted in better growth performance, followed by coco coin, rockwool, and oasis cubes. The experiment results suggested that growing lettuce in a potting mix combined with a 1200 ppm nutrient solution in hydroponic systems significantly enhanced growth and yield.

  PublisherDOI

Recent grants

• SHF: Small: Formalisms, Implementations, and Verification Procedures for Alternatives to Floating Point

  NSF · $516k · 2019–2024

• SHF:Small:Techniques for Generating Correctly Rounded Math Libraries

  NSF · $500k · 2021–2026

• FMitF: Track II: Automated Verification for Assembly Implementations of Cryptography Libraries

  NSF · $100k · 2019–2022

• SaTC: Hardware-Assisted Methods for Operating System Integrity

  NSF · $500k · 2014–2018

• CAREER: Semantics, Abstractions, and Tools for a Pragmatic Verified LLVM Compiler

  NSF · $561k · 2015–2020

Frequent coauthors

• Milo M. K. Martin

  Google (United States)

  19 shared

• Jay P. Lim

  Rutgers, The State University of New Jersey

  19 shared

• Steve Zdancewic

  University of Pennsylvania

  16 shared

• Mohammadreza Soltaniyeh

  Samsung (United States)

  10 shared

• Mridul Aanjaneya

  Rutgers, The State University of New Jersey

  10 shared

• Adarsh Yoga

  9 shared

• Yun Zhao

  8 shared

• David Menendez

  8 shared

Labs

• RAPLPI

  Rutgers Architecture and Programming Languages Research Group

Education

• Ph.D., Computer Science

  Rutgers, The State University of New Jersey

Awards & honors

• Intel Memory Protection Extensions
• 2023 ACM Distinguished Member
• ICSE 2016 Notable Books and Articles of 2016
• PLDI 2015 Distinguished Paper
• PLDI 2021 Distinguished Paper Award