Jean-Baptiste Jeannin

I am an Associate Professor in Aerospace Engineering at the University of Michigan — Ann Arbor, where I lead the MARVL group. I am also affiliated with Computer Science and Engineering and Robotics. During the year 2024-2025 I was on sabbatical in the PARKAS team at École Normale Supérieure.

I received a Ph.D. in Computer Science from Cornell University in 2013, where I was advised by Dexter Kozen, as well as a Diplôme d'Ingénieur from École polytechnique in 2007. I used to be a Researcher at Samsung Research America in Mountain View, California and a Post Doctoral Fellow working with André Platzer at Carnegie Mellon University.

Research Interests

• Verification of cyber-physical systems, in particular aerospace applications
• Verification of numerical methods
• Logics and semantics of programming languages, in particular synchronous languages
• Programming with coinductive types

Graduate Students

• Jiawei Chen (PhD candidate in Robotics)
• Yonathan Fisseha (PhD candidate in Computer Science and Engineering, co-advised with Todd Austin)
• Nishant Kheterpal (PhD candidate in Robotics)
• Yichen Tao (PhD candidate in Computer Science and Engineering)
• Serra Dane (PhD student in Computer Science and Engineering)

Alumni

• Mohit Tekriwal (PhD 2023 in Aerospace Engineering, now research scientist at Lawrence Livermore National Labs)
• Hammad Ahmad (PhD 2024 in Computer Science and Engineering, co-advised with Wes Weimer, now assistant teaching professor at Carnegie Mellon University)
• Elanor Tang (MS 2024 in Computer Science and Engineering, now PhD student at Carnegie Mellon University)

Publications

• Automatic Certification of the Active Corner Method for Collision Avoidance. Nishant Kheterpal, J. Tanner Slagel, Elanor Tang, Serra Dane and Jean-Baptiste Jeannin. In NASA Formal Methods (NFM 2026), to appear.

• Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types. Serra Dane, Jiawei Chen, Marc Pouzet and Jean-Baptiste Jeannin. In NASA Formal Methods (NFM 2026), to appear.

• Provably Safe Optimization of Arrival Flows into Terminal Airspace. Serra Dane, Kuang Sun, Yuwei Hu, Eric Boccaccio, Adrian Nomi, Joshua H. Glottmann, Jean-Baptiste Jeannin and Max Z. Li. In AIAA Aviation 2026, to appear.

• A General Framework for Robust Quantitative Semantics of Signal Temporal Logic. Jiawei Chen, José Luiz Vargas de Mendonça, Konstantinos Mamouras and Jean-Baptiste Jeannin. In Formal Methods (FM 2026). [full text (.pdf)]

• Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities. Yichen Tao, Hongfei Fu, Jiawei Chen and Jean-Baptiste Jeannin. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2026). [full text (.pdf)]

• Formalization of asymptotic convergence for Stationary Iterative Methods. Mohit Tekriwal, Joshua Miller and Jean-Baptiste Jeannin. In NASA Formal Methods (NFM 2024). [full text (.pdf)]

• Formally Verified Asymptotic Consensus in Robust Networks. Mohit Tekriwal, Avi-Tachna Fram, Jean-Baptiste Jeannin, Manos Kapritsos and Dimitra Panagou. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024). [full text (.pdf)]

• Security Verification of Low-Trust Architectures. Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik and Todd Austin. In ACM Conference on Computer and Communications Security (CCS 2023). Distinguished paper award. [full text (.pdf)]

• Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel and Jean-Baptiste Jeannin. In 6th Conference on Intelligent Computer Mathematics (CICM 2023). [full text (.pdf)]

• A Concurrent Switching Model for Traffic Congestion Control. Hossein Rastgofta, Xun Liu and Jean-Baptiste Jeannin. In Modeling, Estimation and Control Conference (MECC 2023). [full text (.pdf)]

• Towards a Study of Performance for Safe Neural Network Training. Nishant Kheterpal and Jean-Baptiste Jeannin. In 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS 2023). [full text (.pdf)]

• How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms. Hammad Ahmad, Zachary Karas, Kimberly Diaz, Amir Kamil, Jean-Baptiste Jeannin, and Westley Weimer. In International Conference on Software Engineering (ICSE 2023). [full text (.pdf)]

• 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 and Jean-Baptiste Jeannin. In Formal Techniques for Safety-Critical Systems (FTSCS 2022). [full text (.pdf)]

• Towards a Formalization of the Active Corner Method for Collision Avoidance in PVS. Nishant Kheterpal and Jean-Baptiste Jeannin. In Formal Techniques for Safety-Critical Systems (FTSCS 2022). [full text (.pdf)]

• Towards Verified Rounding-Error Analysis for Stationary Iterative Methods. Ariel E. Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, and Geoffrey Hulette. In Correctness 2022: Sixth International Workshop on Software Correctness for HPC Applications. [full text (.pdf)]

• Automating Geometric Proofs of Collision Avoidance with Active Corners. Nishant Kheterpal, Elanor Tang and Jean-Baptiste Jeannin. In Formal Methods in Computer-Aided Design (FMCAD 2022). [full text (.pdf)]

• Work-in-Progress: Towards a Theory of Robust Quantitative Semantics for Signal Temporal Logic. Jean-Baptiste Jeannin, Jiawei Chen, José Luiz Vargas de Mendonça and Konstantinos Mamouras. In International Conference on Embedded Software (EMSOFT 2022). [full text (.pdf)]

• Efficient Backward Reachability using the Minkowski Difference of Constrained Zonotopes. In International Conference on Embedded Software (EMSOFT 2022). Liren Yang, Hang Zhang, Jean-Baptiste Jeannin and Necmiye Ozay. [full text (.pdf)]

• Synthesizing Legacy String Code for FPGAs Using Bounded Automata Learning. Kevin Angstadt, Tommy Tracy, Kevin Skadron, Jean-Baptiste Jeannin and Westley Weimer. In IEEE Micro (2022). [full text (.pdf)]

• Twine: a Chisel extension for component-level heterogeneous design. Shibo Chen, Yonathan Fisseha, Jean-Baptiste Jeannin and Todd Austin. In Design Automation & Test in Europe (DATE 2022). [full text (.pdf)]

• Dandelion: Certified Approximations of Elementary Functions. Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova and Jean-Baptiste Jeanninn. In Interactive Theorem Proving (ITP 2022). [full text (.pdf)]

• Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems. Haojun Ma, Hammad Ahmad, Aman Goel, Eli Goldweber, Jean-Baptiste Jeannin, Manos Kapritsos and Baris Kasikci. In Usenix Annual Technical Conference (ATC 2022). [full text (.pdf)]

• A formal proof of the Lax equivalence theorem for finite difference schemes. Mohit Tekriwal, Karthik Duraisamy and Jean-Baptiste Jeannin. In NASA Formal Methods (NFM 2021). [full text (.pdf)]

• A Physics-Based Finite-State Abstrac- tion for Traffic Congestion Control. Hossein Rastgoftar and Jean-Baptiste Jeannin. American Control Conference (ACC 2021). [full text (.pdf)]

• A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems. Hammad Ahmad and Jean-Baptiste Jeannin. Hybrid Systems: Computation and Control (HSCC 2021). [full text (.pdf)] [Extended Technical Report (.pdf)]

• Falsification of a Vision-based Automatic Landing System. Sara Shoouri, Shayan Jalili, Jiahong Xu, Isabelle Gallagher, Joshua Wilhelm, Necmiye Ozay and Jean-Baptiste Jeannin. In AIAA SciTech 2021. [full text (.pdf)]

• Verification of an Airport Taxiway Path-Finding Algorithm. Siyuan He, Ke Du, Joshua Wilhelm and Jean-Baptiste Jeannin. In Digital Aerospace Systems Conference (DASC 2020). [full text (.pdf)]

• An Integrative Behavioral-based Physics-inspired approach to traffic congestion control. Hossein Rastgoftar, Jean-Baptiste Jeannin and Ella Atkins. In Dynamics Systems and Control Conference (DSCC 2020). [full text (.pdf)]

• Formal Verification of Braking while Swerving in Automobiles. Aakash Abhishek, Harry Sood and Jean-Baptiste Jeannin. In Hybrid Systems: Computation and Control (HSCC 2020). [full text (.pdf)]

• Formal Verification of Swerving Maneuvers for Car Collision Avoidance. Aakash Abhishek, Harry Sood and Jean-Baptiste Jeannin. In American Control Conference (ACC 2020). [full text (.pdf)]

• Accelerating Legacy String Kernels via Bounded Automata Learning. Kevin Angstadt, Jean-Baptiste Jeannin and Westley Weimer. In Architectural Support for Programming Languages and Operating Systems (ASPLOS 2020). [full text (.pdf)]

• A Software Architecture for Autonomous Taxiing of Aircraft. Yuhao Zhang, Guillaume Poupart-Lafarge, Huaiyuan Teng, Joshua Wilhelm, Jean-Baptiste Jeannin, Necmiye Ozay and Eelco Scholte. In AIAA SciTech 2020. [full text (.pdf)]

• I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols. Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci and Karem A. Sakallah. In Symposium on Operating Systems Principles (SOSP 2019). [full text (.pdf)]

• Provably Safe Controller Synthesis Using Safety Proofs as Building Blocks. Yanni Kouskoulas, Aurora Schmidt, Jean-Baptiste Jeannin, Daniel Genin and Jessica Lopez. In International Conference on Software Engineering Research and Innovation (CONISOFT 2019). [full text (.pdf)]

• Programming with Rational Coinductive Streams. Jean-Baptiste Jeannin. In Workshop on ML-family Programming Languages (ML 2019). [full text (.pdf)]

• Formal Specification of Continuum Deformation Coordination. Hossein Rastgoftar, Jean-Baptiste Jeannin and Ella M. Atkins. In American Control Conference (ACC 2019). [full text (.pdf)]

• Formal Verification of Collision Avoidance for Turning Maneuvers in UAVs. Eytan Adler and Jean-Baptiste Jeannin. In AIAA Aviation 2019. [full text (.pdf)]

• Towards Automatic Inference of Inductive Invariants. Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci and Karem A. Sakallah. In Workshop on Hot Topics in Operating Systems (HotOS 2019). [full text (.pdf)]

• Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions. Kyle D. Julian, Shivam Sharma, Jean-Baptiste Jeannin and Mykel J. Kochenderfer. In Verification of Neural Networks (VNN 2019). [full text (.pdf)]

• IoTa: A Calculus for Internet of Things Automation. Julie L. Newcomb, Satish Chandra, Jean-Baptiste Jeannin, Cole Schlesinger and Manu Sridharan. In Onward! 2017, part of Systems, Programming, Languages and Applications: Software for Humanity (SPLASH). [full text (.pdf)]

• Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics. Yanni Kouskoulas, Daniel Genin, Aurora Schmidt and Jean-Baptiste Jeannin. In Interactive Theorem Proving (ITP 2017). [full text (.pdf)]

• Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. Andrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin and Martin T. Vechev. In Computer-Aided Verification (CAV 2017). [full text (.pdf)]

• Fission: Dynamic Code Splitting for Javascript. Arjun Guha, Jean-Baptiste Jeannin, Rachit Nigam, Rian Shambaugh and Jane Tangen. In Summit on Advances in Programming Languages (SNAPL 2017). [full text (.pdf)]

• Correct by Construction Networks using Stepwise Refinement. Leonid Ryzhyk, Nikolaj Bjorner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry and George Varghese. In Network Systems Design and Implemention (NSDI 2017). [full text (.pdf)]

• CoCaml: Functional programming with regular coinductive types. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Fundamenta Informaticae (FI), 150:347-377, 2017. [full text (.pdf)] [BibTeX]

• A Formally Verified Hybrid System for Safe Advisories in the Next-Generation Airborne Collision Avoidance System. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Stefan Mitsch and André Platzer. International Journal on Software Tools for Technology Transfer (STTT), 2017. [full text (.pdf)] [BibTeX]

• Type Inference for Static Compilation of JavaScript. Satish Chandra, Colin Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip and Youngil Choi. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2016). [full text (.pdf)]

• Well-founded coalgebras, revisited. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Mathematical Structures in Computer Science (MSCS), FirstView:1-21, February 2016. [journal link] [full text (.pdf)] [BibTeX]

• Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. Invited paper. In International Conference on Embedded Software (EMSOFT 2015). [full text (.pdf)] [BibTeX]

• A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). [full text (.pdf)] [BibTeX]

• dTL²: Differential temporal dynamic logic with nested modalities for hybrid systems. Jean-Baptiste Jeannin and André Platzer. In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Vienna, Austria, July 19-22, 2014, Proceedings, volume 8562 of LNCS, pages 292-306. Springer, 2014. [full text (.pdf)] [BibTeX]

• NetKAT: Semantic foundations for networks. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. In Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL 2014), pages 113-126, San Diego, California, USA, January 2014. ACM. [full text (.pdf)] [BibTeX]

• Hybrid theorem proving of aerospace systems: Applications and challenges. Khalil Ghorbal, Jean-Baptiste Jeannin, Erik P. Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell. Journal of Aerospace Information Systems (JAIS), 11, pp. 702-713. 2014. [full text (.pdf)] [BibTeX]

• Language constructs for non-well-founded computation. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Matthias Felleisen and Philippa Gardner, editors, 22nd European Symposium on Programming (ESOP 2013), LNCS 7792, pp. 61-80. Springer, Heidelberg (2013). [full text (.pdf)] [BibTeX]

• DKAL*: Constructing Executable Specifications of Authorization Protocols. Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg and Nikhil Swamy. In International Symposium on Engineering Secure Software and Systems (ESSoS 2013), February 2013. [full text (.pdf)] [page at Microsoft Research] [BibTeX]

• Computing with Capsules. Jean-Baptiste Jeannin and Dexter Kozen. Journal of Automata, Languages and Combinatorics (JALC), 17(2-4):185-204, 2012. [full text (.pdf)] [BibTeX]

• Computing with Capsules. Jean-Baptiste Jeannin and Dexter Kozen. In Martin Kutrib, Nelma Moreira, and Rogério Reis, editors, Proc. Conf. Descriptional Complexity of Formal Systems (DCFS 2012), volume 7386 of Lecture Notes in Computer Science, pages 1-19, Braga, Portugal, July 2012. Springer. (Subsumed by Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. J. Automata, Languages and Combinatorics, 17(2-4):185-204, 2012.) [BibTeX]

• Capsules and Separation. Jean-Baptiste Jeannin and Dexter Kozen.In Nachum Dershowitz, editor, Proc. 27th ACM/IEEE Symp. Logic in Computer Science (LICS 2012), pages 425-430, Dubrovnik, Croatia, June 2012. IEEE. [full text (.pdf)] [BibTeX]

• Capsules and Closures: a Small-Step Approach. Jean-Baptiste Jeannin. In Robert L. Constable and Alexandra Silva, editors, Logic and Program Semantics, Essays Dedicated to Dexter Kozen on the Occasion of his 60th Birthday. [full text (.pdf)] [BibTeX]

• Capsules and Closures. Jean-Baptiste Jeannin. In Michael Mislove and Joël Ouaknine, editors, Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXVII), pages 191-213, Pittsburgh, PA, May 2011. Elsevier Electronic Notes in Theoretical Computer Science. [full text (.pdf)] [BibTeX]

• Formal Verification of Safety Buffers for State-Based Conflict Detection and Resolution. Heber Herencia-Zapana, Jean-Baptiste Jeannin, César Muñoz. Proceedings of the 27th International Congress of the Aeronautical Sciences (ICAS 2010), 2010. [full text (.pdf)] [BibTeX]

Thesis

• Capsules and Non-Well-Founded Computation. PhD thesis, Cornell University, August 2013. [full text (.pdf)]

Projects

• Capsules
• CoCaml
• MARVeLus, a refinement-type verification system for synchronous languages
• Verinum, verification of numerical methods

Teaching

I am or have been the instructor for:

• AERO 552 Aerospace Information Systems in Fall 2017, Winter 2019, Winter 2021, Winter 2022, Fall 2023, and Fall 2025 (University of Michigan);
• AERO 350 (formerly AERO 495) Fundamentals of Aerospace Computing in Fall 2018, Fall 2019, Fall 2020, Fall 2021, Fall 2022, Winter 2023, and Winter 2026 (University of Michigan);
• EECS 590 Advanced Programming Languages in Winter 2020, Fall 2022 and Winter 2024 (University of Michigan).