Formal Verification for Numerical Methods
The goal of this project is to develop an end-to-end verification framework for numerical programs. We use a formal methods tool called Coq proof assistant to write formal specifications for the behavior of numerical algorithms and prove accuracy and correctness of the algorithm. This work takes into account the effect of finite precision on the behavior of numerical algorithms.
Papers:
- Formal verification of iterative convergence of numerical algorithms. Mohit Tekriwal, Joshua Miller, and Jean-Baptiste Jeannin.
- Dandelion: Certified Approximations of Elementary Functions. Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin.
- A formal proof of the Lax equivalence theorem for finite difference schemes. Mohit Tekriwal, Karthik Duraisamy, and Jean-Baptiste Jeannin.
- Towards Verified Rounding-Error Analysis for Stationary Iterative Methods. Ariel Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, Geoffrey Hulette.
Synchronous Programming with Verification for Robotics
Papers:
- Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation. Jiawei Chen, José Luiz Vargas de Mendonça, Shayan Jalili, Bereket Shimels Ayele, Bereket Ngussie Bekele, Zhemin Qu, Pranjal Sharma, Tigist Shiferaw, Yicheng Zhang, Jean-Baptiste Jeannin.
Automatic Verification for Collision Avoidance
Watch a video on our work (presented at FMCAD ’22) below.
Papers:
- Automating Geometric Proofs of Collision Avoidance with Active Corners. Nishant Kheterpal, Elanor Tang, and Jean-Baptiste Jeannin.
- Towards a Formalization of the Active Corner Method for Collision Avoidance in PVS. Nishant Kheterpal and Jean-Baptiste Jeannin.
Formal verification applied to control theory
Papers:
- Formally verified asymptotic consensus in robust networks. Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou.