Debasmita Lohar

Debasmita Lohar

PhD Student

The true measure of success is how many times you can bounce back from failure.  - Stephen Richards
Contact Me

About Me

Hello! I am a PhD student under the supervision of Dr. Eva Darulova at Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany.

My primary research areas are: Program Analysis, Approximate Computing, Probabilistic Analysis.

Prior to this, I have completed Master of Science (MS) by Research under the supervision of Dr. Soumyajit Dey in the Department of Computer Science & Engineering of Indian Institute of Technology, Kharagpur, India.

Research Activities


  • In July, I am joining Microsoft Research Lab India as a Research Intern.

  • I am on the TACAS'22 Artifact Evaluation Committee.

  • Our tool Blossom is now available on GitHub.

  • Research Tools

  • Blossom: A framework for fuzzing numerical programs

  • Daisy: A framework for verifying and optimizing numerical programs

  • ProPFA: Probabilistic Path-based Failure Analyzer

  • MS Thesis

    Formal Methods for Probabilistic Failure Analysis of Behavioral Specifications

    Download Thesis


    • A Two-Phase Approach for Conditional Floating-Point Verification, Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, and Maria Christakis, TACAS 2021. (Paper) (Talk)

    • Sound Probabilistic Numerical Error Analysis, Debasmita Lohar, Milos Prokop, and Eva Darulova, iFM 2019. (Paper) (Presentation)

    • Discrete Choice in the Presence of Numerical Uncertainties, Debasmita Lohar, Eva Darulova, Sylvie Putot, and Eric Goubault, ESWEEK-TCAD special issue 2018. (Paper) (Presentation)

    • Work-in-Progress: Verifying Stability Guarantees of Control Software Implementations in the Presence of Sensor Level Faults, Saurav Kumar Ghosh, Debasmita Lohar, Dibyendu Das, and Soumyajit Dey, EMSOFT 2017. (Paper)

    • Failure Estimation of Behavioral Specifications, Debasmita Lohar, Anudeep Dunaboyina, Dibyendu Das, and Soumyajit Dey, SETTA 2016. (Paper)

    • Integrating Formal Methods with Testing for Reliability Estimation of Component Based Systems, Debasmita Lohar and Soumyajit Dey, ISSRE 2015. (Paper)

    View on DBLP

    Selected Projects

    Memory Safety Verification of FreeRTOS protocols

    Automated Reasoning Group, Amazon Web Services (AWS), Boston, United States
    Supervisor: Mark Tuttle
    Duration: May 2019 - July 2019

    This project was focused on verifying memory safety of network protocols of Amazon's FreeRTOS using Bounded Model Checking (blog post). All proofs are available on Github.

    Automated Verification and Approximation

    Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany
    Supervisor: Dr. Eva Darulova
    Duration: July 2016 - September 2016

    The motivation of this project was to statically infer properties of a program in presence of imprecise probabilistic inputs. The probabilistic analysis can be found on Github.

    RTOS Validation and Development Support

    Indian Institute of Technology (IIT), Kharagpur, India
    Supervisors: Prof. (Dr.) Pallab Dasgupta and Dr. Soumyajit Dey
    Sponsor: Hindustan Aeronautics Limited
    Duration: October 2015 - June 2016

    This project was focused on formal verification of a real time operating system of a safety critical avionic system.

    Architecture and Algorithmic Optimizations for Speech based Communication Interfaces on Mobile Devices

    Indian Institute of Technology (IIT), Kharagpur, India
    Supervisor: Dr. Soumyajit Dey
    Sponsor: Intel Semiconductor (US) Limited
    Duration: September 2013 - January 2016

    The main objective of this project was to present a hardware-software co-processing speech recognizer where the hardware accelerator would accelerate computationally intensive parts of the algorithm.

    web counter free