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
June, 2024: Our paper titled " Design and implementation of a verified interpreter for additive manufacturing programs" has
been accepted for publication in FUNCARCH, 2024,
co-located with ICFP, 2024.
Feb, 2024: Our paper titled "Formalization of asymptotic convergence for Stationary Iterative Methods" has been
accepted for publication in NFM, 2024.
Dec, 2023: Our paper titled "Formally verified asymptotic consensus in robust networks" has been
accepted for publication in TACAS, 2024.
June 2023 -
Defended my PhD thesis, titled "A Mechanized Error Analysis Framework for End-to-End Verification of Numerical Programs
Our paper titled "LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs" was accepted at
the ARITH, 2023 conference.
May, 2023: Our paper titled "Verified Correctness, Accuracy, and Convergence of a Stationary Interative Linear Solver: Jacobi Method"
has been accepted at the CICM, 2023 conference.
Oct, 2022 - Jan, 2023: Visited the STAMP team in INRIA, Sophia Antipolis, France.
Sept, 2022- Our paper titled "Towards Verified Rounding-Error Analysis for Stationary Iterative Methods" has been accepted at
the Correctness,2022 workshop
May, 2022- Selected for the prestigious Chateaubriand fellowship
to conduct a part of my PhD research at INRIA, France.
We would once again like to congratulate this
years group of Chateaubriand STEM Fellowship recipients! You can find this years list of laureates on our website
here -->https://t.co/pnXx1hp1yd
—
ChateaubriandProgram (@ChateaubriandUS) June 9, 2022
[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
Addressed challenges associated with feedback flow control that include development of an effective and robust control law, and development of small and reliable actuators
Implemented Genetic Algorithm (GA) based techniques to find optimal values of PID control law constants that suppress energetic velocity modes and reduce drag in turbulent flows
Fabricated a prototype of a piston-based actuator using 3-D printing
Employed scotch-yoke mechanism in the actuator to convert rotary motion of the motor shaft to linear motion of the piston
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
Simulated and analyzed flow in a 2D Lid Driven Cavity
Successfully obtained a narrow range of optimal excitation amplitude responsible for onset of temporal instabilities in the system for Reynolds number in the range: 8000 - 8660
Carried Flow visualization studies and post processing using TecPlot
Redrew bifurcation curve using vorticity time series data with respect to specific numerical method to obtain reported critical Reynolds number by other researchers
Extended the exercise for 257 x 257 grid to finer grids: 513 x 513 and 1025 x 1025, and obtained similar results
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)
2024
Matthew Sottile, Mohit K. Tekriwal.
" Design and implementation of a verified interpreter for additive manufacturing programs".
[pdf] In the ACM SIGPLAN workshop for functional software architecture (FUNARCH), 2024.
(co-located with ICFP, 2024)
Mohit K. Tekriwal, Joshua Miller, Jean-Baptiste Jeannin.
"Formalization of asymptotic convergence for Stationary Iterative Methods".
[pdf]In the NASA Formal Methods (NFM), 2024
Mohit K. Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou.
"Formally verified asymptotic consensus in robust networks". In the
30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2024.[pdf]
2023
Mohit K. Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin.
"Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method".
In 16th Conference on Intelligent Computer Mathematics, 2023[pdf]
Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, David Bindel.
"LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs".
In 30th IEEE International Symposium on Computer Arithmetic, 2023[pdf]
2022
Heiko Becker, Mohit K. Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin.
"Dandelion: Certified Approximations of Elementary Functions". In Thirteenth Conference on Interactive Theorem Proving, 2022[pdf]
Mohit K. Tekriwal[*], Ariel Kellison[*], Jean-Baptiste Jeannin, Geoffrey Hulette.
"Towards Verified Rounding-Error Analysis for Stationary Iterative Methods". In Software Correctness workshop for high performance computing[pdf] ([*]: equal contribution)
2021
Mohit K. Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin.
"A formal proof of the Lax equivalence theorem in finite difference schemes". In 13th NASA Formal Methods Symposium, 2021.
[pdf][cite].
2019
V. K. Suman, Siva Viknesh S.,Mohit K. Tekriwal, Swagata Bhaumik, Tapan K. Sengupta.
"Grid sensitivity and role of error in computing a lid-driven cavity problem". In Phys. Rev. E 99, 013305. (2019)DOI[pdf][cite].