Projects

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:

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:

Formal verification applied to control theory

Papers: