360 Huntington Avenue
330 West Village H
Boston, MA 02115
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.
- MTech in Computer Science and Engineering, Indian Institutes of Technology Bombay – India
- BE in Computer Engineering, University of Mumbai – India
- Hometown: Mumbai, India
- Field of Study: Formal Methods
- PhD Advisor: Thomas Wahl
What are the specifics of your graduate education (thus far)?
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.
What are your research interests?
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.
What’s one problem you’d like to solve with your research/work?
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.
What aspect of what you do is most interesting?
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.
What are your research or career goals, going forward?
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.