![Jaideep Ramachandran](https://s32615.pcdn.co/wp-content/uploads/2022/01/Jaideep-Ramachandran-hero-image2880x956-scaled.jpg)
![Need to add an ALT text field to the CMS for the Hero Image](https://s32615.pcdn.co/wp-content/uploads/2022/01/Jaideep-Ramachandran-hero-mobile640x390.jpg)
Jaideep Ramachandran
![Jaideep Ramachandran](https://s32615.pcdn.co/wp-content/uploads/2022/01/Jaideep-Ramachandran-hero-image2880x956-scaled.jpg)
![Jaideep Ramachandran](https://s32615.pcdn.co/wp-content/uploads/2022/01/Jaideep-Ramachandran-hero-mobile640x390.jpg)
Jaideep is a PhD student in the formal methods group at Northeastern University’s Khoury College of Computer Sciences, advised by Professor Thomas Wahl. His research lies broadly in the area of mechanized formal/semi-formal verification of systems. He works on developing techniques and tools to automatically reason about computations involving floating-point numbers. As part of his dissertation research, he is currently working on designing, implementing and evaluating an abstraction-refinement type approach to solve floating-point constraints. During the course of his graduate education, he has done internships at SGT Inc. in the Robust Software Engineering group at NASA Ames Research Center, and in the Simulink Design Verifier team at Mathworks Inc. He has served a sub-reviewer for research conferences in formal methods like Computer Aided Verification, Formal Methods in Computer Aided Design, and Tools & Algorithms for Construction and Analysis of Systems. Before joining Northeastern, Jaideep worked at Samsung as a software developer writing software for mobile phones. He holds a master’s degree in computer science and engineering from Indian Institutes of Technology Bombay, India, and a bachelor’s degree in computer engineering from the University of Mumbai in India.
My current work also involves designing, implementing and evaluating an abstraction-refinement type approach to solve floating-point constraints. Earlier, as part of the same project, we developed an encoding of floating-point arithmetic using Reals and Integers, that could leverage existing SMT solvers to solve the resulting 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.
My research is part of the effort of the formal methods and software engineering communities to make software more reliable. A very satisfying aspect about working in the area of formal methods is that there is a good way to strike a balance between theory and practice – the results of theoretical work can be applied to design and reason about practical software and hardware systems in a rigorous fashion.
I would like to take the uncertainty and mystery out of writing numerical programs, so that we are assured that the systems using floating-point numbers that we use and rely upon behave in a predictable way.
The most interesting fact is that although software and computers have become so ubiquitous and an integral part of our lives, all software exhibit unexpected behavior under certain circumstances – the consequence of such erratic behavior can range from being totally benign to annoying (computer slowing down or crashing) to catastrophic (space shuttles coming down). We still do not have a clear way to guarantee that safety/mission critical software satisfy their functional requirements under all conditions.
I would like to see techniques developed by the formal methods academic and research community make their way into products and improving software engineering processes in industry, and aim to be a part of that effort.
Jaideep is a PhD student in the formal methods group at Northeastern University’s Khoury College of Computer Sciences, advised by Professor Thomas Wahl. His research lies broadly in the area of mechanized formal/semi-formal verification of systems. He works on developing techniques and tools to automatically reason about computations involving floating-point numbers. As part of his dissertation research, he is currently working on designing, implementing and evaluating an abstraction-refinement type approach to solve floating-point constraints. During the course of his graduate education, he has done internships at SGT Inc. in the Robust Software Engineering group at NASA Ames Research Center, and in the Simulink Design Verifier team at Mathworks Inc. He has served a sub-reviewer for research conferences in formal methods like Computer Aided Verification, Formal Methods in Computer Aided Design, and Tools & Algorithms for Construction and Analysis of Systems. Before joining Northeastern, Jaideep worked at Samsung as a software developer writing software for mobile phones. He holds a master’s degree in computer science and engineering from Indian Institutes of Technology Bombay, India, and a bachelor’s degree in computer engineering from the University of Mumbai in India.
My current work also involves designing, implementing and evaluating an abstraction-refinement type approach to solve floating-point constraints. Earlier, as part of the same project, we developed an encoding of floating-point arithmetic using Reals and Integers, that could leverage existing SMT solvers to solve the resulting 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.
My research is part of the effort of the formal methods and software engineering communities to make software more reliable. A very satisfying aspect about working in the area of formal methods is that there is a good way to strike a balance between theory and practice – the results of theoretical work can be applied to design and reason about practical software and hardware systems in a rigorous fashion.
I would like to take the uncertainty and mystery out of writing numerical programs, so that we are assured that the systems using floating-point numbers that we use and rely upon behave in a predictable way.
The most interesting fact is that although software and computers have become so ubiquitous and an integral part of our lives, all software exhibit unexpected behavior under certain circumstances – the consequence of such erratic behavior can range from being totally benign to annoying (computer slowing down or crashing) to catastrophic (space shuttles coming down). We still do not have a clear way to guarantee that safety/mission critical software satisfy their functional requirements under all conditions.
I would like to see techniques developed by the formal methods academic and research community make their way into products and improving software engineering processes in industry, and aim to be a part of that effort.