Jaideep Ramachandran
Mail address: 202 West Village H, 440 Huntington Avenue, Boston, MA 02115
Email address: <my-firstname-then-obvious-symbol>ccs.neu.edu

I am working on a Ph.D. in Computer Science, at 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 currently analyzing Floating point operations in OpenCL programs, investigating the twin challenges of concurrency and 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 decsiion procedures for Reals and Integers. More details here. 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.

Before joining Northeastern, I worked at Samsung as a software developer writing software for mobile phones. Even before that, I was a student in the Computer Science and Engineering department at IIT Bombay, from where I graduated with a master's degree, advised by Prof. Supratik Chakraborty. I was also affiliated to the Center for Formal Design and Verification of Software at IIT Bombay.

Papers:

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