Jaideep Ramachandran
Email address: <my-firstname-then-obvious-symbol>ccs.neu.edu

I am a graduate student in the College of Computer and Information Science, Northeastern University, Boston advised by Prof. Thomas Wahl. I am a member of the Formal Methods group. My research focusses on mechanized formal/semi-formal verification of systems. I am working on developing tools for automatically analyzing floating-point operations, investigating the intricacies of floating-point arithmetic in programs running on heterogeneous systems. In particular, I am developing a decision procedure for an interesting fragment of floating-point arithmetic, but by reasoning at a level much higher than the bit-level: using decision procedures for Reals and Integers. My current work also involves designing, implementing and evaluating an abstraction-refinement type approach to solve non-linear floating-point constraints. 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.

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.

I graduated with a Master's degree in Computer Science and Engineering from IIT Bombay. I also 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.


  1. 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): 1-5(2015).
  2. 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.
  3. 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].
  4. Zahra Jafargholi, Hamidreza Jahanjou, Eric Miles, Jaideep Ramachandran, Emanuele Viola. From RAM to SAT. Electronic Colloquium on Computational Complexity (ECCC) 19: 125 (2012). [Paper].

Professional Service: I have been a sub-reviewer for CAV'15, FMCAD'14, CAV'14, DATE'14, ICFPT'13, ASE'13, FMCAD'13, CAV'13, DATE'13, TACAS'12, FMCAD'12, MEMOCODE'12.