Mohit Tekriwal
PhD Candidate, Department of Aerospace Engineering, University of Michigan  Ann Arbor
I am currently a PhD candidate in the
Department of Aerospace engineering at the
University of Michigan. I am advised by
Prof. JeanBaptiste Jeannin.
I completed my masters in
Aerospace engineering at the University of Michigan in 2020.
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 FramaC/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

Oct, 2022  Jan, 2023: Visited the STAMP team in INRIA, Sophia Antipolis, France.

Sept, 2022 Our paper titled "Towards Verified RoundingError 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.

April, 2022 

March, 2022  Our paper titled "Dandelion: Certified Approximations of Elementary Functions" got accepted at
the Thirteenth Conference on Interactive Theorem Proving, 2022

June, 2021  August, 2021  Interned at the Max Planck Institute for Software Systems under the supervision of
Prof. Eva Darulova

May, 2021  Presented my paper titled "A formal proof of the Lax equivalence theorem in finite difference schemes" at the
NASA Formal Methods conference (NFM), 2021

May, 2020  Advaced to PhD candidacy in Aerospace engineering at the University of Michigan, Ann Arbor

April, 2020  Received a Masters degree in Aerospace engineering at the University of Michigan, Ann Arbor

September, 2018  Joined the PhD program at the University of Michigan, Ann Arbor

June, 2018  Graduated from the Indian Institute of Technology (IIT), Kanpur with Bachelors in Aerospace engineering
Research in formal methods applied to numerical analysis
Formal Verification of Numerical schemes (2018  Present)
Advisor: Prof. JeanBaptiste Jeannin, Department of Aerospace engineering, University of Michigan, Ann Arbor

Learnt functionalities of Coq proof assistant

Formally verified consistency of a 2nd order central finite difference scheme in Coq proof assistant

Formalized the Laxequivalence theorem (statement of convergence of finite difference schemes) in the Coq Proof assistant

Formally verified stability of Forward in time and Central in Space (FTCS) scheme for 1Dheat diffusion equation

Explored light weight verification techniques like FramaC to carry verification at the code level

Formalized the convergence of classical iterative methods in the Coq proof assistant
Verified QR factorization algorithm (June 2022  Present)
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 (MPISWS),
currently at the University of Uppsala

Worked on formalization of the Remez algorithm for approximation of transcendental functions in HOL4 theorem prover

Implemented the first version of certificate checker in a static analysis tool, Daisy

Formalized the McLaurin series approximation of transcendental functions and root finding methods in HOL4 theorem prover
Verification of the WeightedMeanSubsequenceReduced (WMSR) algorithm (June 2021  Present)
[1] Department of Aerospace engineering, University of Michigan, Ann arbor
[2] Department of Electrical engineering and Computer Science, University of Michigan, Ann arbor
WMSR 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 pistonbased actuator using 3D printing

Employed scotchyoke 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)