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. 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. My advisor is Prof. Thomas Wahl. 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. My mentor was Dr. Corina Păsăreanu.
I graduated with a Master's degree in Computer Science and Engineering from IIT Bombay. My advisor was Prof. Supratik Chakraborty. 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.
- 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): 1-5(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 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.