Jean-Baptiste Jeannin
Assistant Professor
Aerospace Engineering
University of Michigan


Software is increasingly present in our transportation systems, from the cars we drive to work to the aircraft we (used to) fly across the country. One particular aspect of this software is that it is often safety-critical, meaning that a serious bug in the software could lead to damage to the vehicle or even loss of life. For this reason the most critical software – such as collision avoidance software – must be thoroughly verified and validated. Formal verification provides a computer-checked proof that the software satisfies a given property, thus providing the highest level of verification and validation. In this talk I will show some recent results of my group on formally verifying several algorithms from the automobile and aerospace industries. I will first present a formal verification of several maneuvers for car collision avoidance, including turning-only maneuvers and braking-while-swerving maneuvers. I will then show how to verify recent designs of aircraft collision avoidance systems that use neural networks, and how to better design them so they don't exhibit bugs. Finally, I will show how to bring formal verification to computational science, with a verification of the Lax theorem for finite difference schemes.

About the speaker...

Jean-Baptiste Jeannin is an Assistant Professor in the Department of Aerospace Engineering at the University of Michigan, Ann Arbor. His research focuses on formal verification of cyber-physical systems and computational schemes, particularly applied to aerospace systems, as well as design and analysis of programming languages. Prior to Michigan, he was a Researcher at Samsung Research America and a Postdoctoral Fellow at Carnegie Mellon University, working with André Platzer. He received his Ph.D. in Computer Science from Cornell University in 2013, where he was advised by Dexter Kozen.