Mohit Tekriwal

Lawrence Livermore National Laboratory, Livermore, CA

Email: tekriwal1@llnl.gov   Ph: +1 734-881-3657   Google Scholar   LinkedIn  Twitter  CV/Resume

I am currently a postdoctoral researcher at the Lawrence Livermore National Labs, working on the application of formal methods to high performance computing. I recently defended my PhD thesis titled "A Mechanized Error Analysis Framework for End-to-End Verification of Numerical Programs" at the University of Michigan. I was advised by Prof. Jean-Baptiste Jeannin. I completed my masters in Aerospace engineering at the University of Michigan in 2020, with speciciality in control theory. I received a bachelors degree in Aerospace engineering from the Indian Insitute of Technology(IIT), Kanpur, India in 2018. My research interests are formal methods, programming languages, numerical analysis and control theory. I am interested in analyzing the accuracy and convergence properties of numerical schemes. I work with interactive theorem provers like Coq Proof assistant, HOL4, to formalize numerical approximation errors and bound them formally. I am also interested in automated reasoning using SMT/SAT solvers and use light weight code analysis tools like Frama-C/VST to certify results obtained from numerical programs.

During my PhD, my research activity has mostly been aligned in the direction of applying formal methods to problems in numerical analysis and control theory. I have been working at the intersection of formal methods and Computational mechanics (my undergraduate coursework and research has primarily been in this field).

Besides research I enjoy outdoor activities like Kayaking, hiking etc. I like to workout and spend time with nature. I also like to go on road trips and enjoy rock music. I like to collect vinyl records. I am a huge fan of the AC/DC, Beatles and Deep Purple.

Updates

Research in applied formal methods

Verified interpreter for 3D printing (Oct, 2023 - Present)

Lawrence Livermore National Laboratory

Formal Verification of Numerical schemes and programs (2018 - 2023)

Advisor: Prof. Jean-Baptiste Jeannin, Department of Aerospace engineering, University of Michigan, Ann Arbor

A peek into my PhD dissertation


Verified QR factorization algorithm (June 2022 - August 2022)

Sandia National Laboratories

  • Wrote a functional model for QR factorizatiom algorithm in Coq
  • Verified properties of correctness for the functional model

    • Certified approximation of Transcendental functions (June 2021 - February 2022)

    Advisor: Prof. Eva Darulova, formerly at the Max Plank Institute for Sofware Systems (MPI-SWS), currently at the University of Uppsala

    Verification of the Weighted-Mean-Subsequence-Reduced (W-MSR) algorithm (June 2021 - February 2022)

    Advisors: Prof. Jean-Baptiste Jeannin [1], Prof. Manos Kapristos[2], Prof. Dimitra Panagou [1]

    [1] Department of Aerospace engineering, University of Michigan, Ann arbor

    [2] Department of Electrical engineering and Computer Science, University of Michigan, Ann arbor

    W-MSR algorithm is a consensus algorithm in controls. We are working on verification of a theorem in the Coq proof assistant, that provides sufficient and necessary conditions for a distributed control systems to reach consensus. We specifically look at a case where there are atmost F malicious nodes in the system that can disrupt information flow between uncorrupted nodes in the network.

    Research in Computational Fluid Dynamics

    Active Flow Control for Drag Reduction in wall bounded Turbulent (May 2017 - July 2017)

    Advisor: Prof. Mitul Luhar, Department of Aerospace and Mechanical engineering, University of Southern California, USA

    Instability and receptivity studies in Lid Driven Cavity Problem (September 2017 - April 2018)

    Advisor: Prof. Tapan K Sengupta, former faculty at the Indian Institute of Technology, Kanpur, India

    Teaching experience

    I was a Graduate Teaching Assistant(GSI) for the course AERO 495 (Fundamentals of Aerospace Computing) in the Fall 2019 and Fall 2020 semesters. This course is an introduction to programming in C, computational sciences and embedded systems. I was responsible for conducting labs, grading homeworks and exams, holding office hours.

    Student feedback rating: 4.6/5.0 (Fall 2020)

    2025

    2024

    2023

    2022

    2021

    2019