After completing my Ph.D., I joined a Formal Verification Center of Expertise at Intel in Hillsboro, Oregon. I work on formally verifying datapaths of microprocessors. These are typically complex arithmetic units within the execution cluster of a processor core, e.g., a unit performing packed Fused-Multiply-Add operations, that have a large input data space, with multiple operations sharing the same hardware, and the circuit being optimized based on latency, power and area considerations. A nice overview of the deployed formal verification technology can be found here.
I was a graduate student in the (Khoury) College of Computer and Information Science, Northeastern University, Boston. I was a member of the Formal Methods group. My research focused on mechanized formal/semi-formal verification of systems.
I have worked on developing tools for automatically analyzing floating-point operations, investigating the intricacies of floating-point arithmetic in programs. In particular, I developed solvers for an interesting fragment of floating-point arithmetic. Some of this was accomplished by reasoning at a level much higher than the bit-level: using solvers/decision procedures for Reals and Integers.
I designed, implemented and evaluated an abstraction-refinement type approach to solve non-linear floating-point formulas, that formed the basis for my doctoral dissertation. An interesting aspect of this approach was that it involved "approaching" the floating-point precision of interest from opposite ends of the precision spectrum: from the "infinitely" precise reals on one side, and lower precision floating-point itself, on the other. My thesis advisor was Prof. Thomas Wahl.
Summer 2015: I was an intern in the Simulink Design Verifier team at Mathworks, Inc .
Summer 2013: I was an intern with SGT, Inc. in the Robust Software Engineering Group at NASA Ames Research Center, where I worked on providing floating-point support for the symbolic execution engine of Java Pathfinder. My mentor was Dr. Corina Păsăreanu.
In the past, I have worked on path interpolation for formulas in the context of loop invariant generation for proving program correctness, and on reachability analysis of large, untimed sequential circuits.
I graduated with a Master's degree in Computer Science and Engineering from IIT Bombay. My advisor was Prof. Supratik Chakraborty. I hold a Bachelor's degree in Computer engineering from the University of Mumbai.
Before joining Northeastern, I worked at Samsung as a software developer writing software for mobile phones.
Papers:
Professional Service: I have been a reviewer for CAV'17, CAV'15, FMCAD'14, CAV'14, DATE'14, ICFPT'13, ASE'13, FMCAD'13, CAV'13, DATE'13, TACAS'12, FMCAD'12, MEMOCODE'12.
A standardized webpage from the College can be found here.
* last updated: 12th March, 2019