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 Prof. Dr. Eva Darulova.

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

Research Activities

News

  • I have successfully defended my thesis on March 27th. The presentation slides are available here.

  • Our tool Aster is now available on GitHub and Zenodo.

    • Research Tools

  • Aster: A mixed fixed-point quantizer for fully connected feed-forward neural networks

  • Blossom: A framework for fuzzing numerical programs

  • PrAn: A tool to capture the effects of probabilistic inputs on numerical programs

  • ProPFA: Probabilistic Path-based Failure Analyzer

    • PhD Thesis

    Expanding the Horizons of Finite-Precision Analysis

    Download Thesis

    MS Thesis

    Formal Methods for Probabilistic Failure Analysis of Behavioral Specifications

    Download Thesis

    Publications

    • 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