Debasmita Lohar

Debasmita Lohar

Postdoctoral Researcher



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 Postdoctoral Researcher in the Application-oriented Formal Verification group led by Prof. Dr. Bernhard Beckert at KASTEL -- Institute of Information Security and Dependability, Karlsruhe Institute of Technology.

I did my PhD at Saarland University in collaboration with the Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, under the supervision of Assoc. Prof. Dr. Eva Darulova.

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

News

  • Our paper Towards Precision-Aware Safe Neural-Controlled Cyber-Physical Systems has been accepted at EMSOFT 2024 Late-Breaking Results.

  • I will give a talk at KeY Symposium on Practical Analysis and Optimization for Finite-Precision.

  • I will be presenting Aster, the Sound Mixed Fixed-Point Quantizer for Neural Networks at the FPtalks Community Meeting on August 8th.

    • Publications

    • Towards Precision-Aware Safe Neural-Controlled Cyber-Physical Systems, Harikishan T S, Sumana Ghosh, and Debasmita Lohar, ESWEEK-ESL special issue 2024. (Preprint)

    • Sound Mixed Fixed-Point Quantization of Neural Networks, Debasmita Lohar, Clothilde Jeangoudoux, Anastasia Volkova, and Eva Darulova, ESWEEK-TECS special issue 2023. (Paper) (Presentation)

    • 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