Welcome to the homepage of Jaideep Ramachandran

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:

• Jaideep Ramachandran and Thomas Wahl. Integrating Proxy Theories and Numeric Model Lifting for Floating-Point Arithmetic. In the Proceedings of Formal Methods in Computer-Aided Design, Mountain View, CA, 2016. [Paper].
• Jaideep Ramachandran, Corina Pasareanu and Thomas Wahl. Symbolic execution for checking the accuracy of floating-point programs. In ACM SIGSOFT Software Engineering Notes 40(1), 2015. [Paper].
• Miriam Leeser, Saoni Mukherjee, Jaideep Ramachandran and Thomas Wahl. Make it Real: Effective Floating-Point Reasoning via Exact Arithmetic. In the Proceedings of Design Automation and Test in Europe (DATE'14), Dresden, Germany, 2014. [Paper].
• Miriam Leeser, Jaideep Ramachandran, Thomas Wahl, and Devon Yablonski. OpenCL floating point software on heterogeneous architectures - portable or not? In the Workshop on Numerical Software Verification (NSV'12), Berkeley, CA, 2012. [Paper].

• With NEU. From RAM to SAT. Electronic Colloquium on Computational Complexity (ECCC) 19: 125 (2012). [Paper].

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