Jean-Baptiste Jeannin

Prof. Jeannin’s research focuses on formal verification in several different areas (cyber-physical systems, scientific computing, distributed systems, computer hardware), with a particular focus on aerospace software systems. On the theoretical side, he develops proof techniques for interactive theorem provers, in order to achieve strong correctness guarantees on critical software systems. He is interested in studying and designing the right formalisms, abstractions and programming languages for programming cyber-physical systems, in particular synchronous languages. On the applications side, he is primarily focused on verifying aerospace and automotive applications for collision avoidance, self-taxiing, and autonomous landing. Over the last few years he has started a research program applying formal verification to scientific computing, providing formally verified approximations of the solutions of differential equations, and computer-checked proof of the correctness, accuracy, and convergence of those solutions.