- Ph.D. Computer Science, Cornell University, 2013
- M.Eng. Computer Science, Cornell University, 2008
- Diplôme d’Ingénieur, École Polytechnique, France, 2007
AERO 552 Aerospace Information Systems, Fall 2017
Research Interests: ^top
- Formal verification of cyber-physical systems
- Aerospace software systems
- Logics and semantics of programming languages
- Programming with coinductive types
- Software security
Jean-Baptiste Jeannin is an Assistant Professor in the Department of Aerospace Engineering at the University of Michigan – Ann Arbor, where his research focuses on formal verification and safety of cyber-physical systems, with a focus on aerospace software systems. His background is in programming languages, logic and security, whose techniques and ideas he applies to the aerospace domain.
Positions Held at UM
Assistant Professor, Aerospace Engineering, 2017 to present
Honors and Awards
Acheson Award 2007, full tuition fellowship at Cornell University
Member of the Association for Computing Machinery (ACM)
Refereed Journal Publications
- Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. CoCaml: Programming with coinductive types. Fundamenta Informaticae (FI), 2017.
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Stefan Mitsch and André Platzer. A Formally Verified Hybrid System for Safe Advisories in the Next-Generation Airborne Collision Avoidance System. International Journal on Software Tools for Technology Transfer (STTT), 2016. Journal extension of our TACAS 2015 paper, invited to special issue.
- Jean-Baptiste Jeannin, Dexter Kozen and Alexandra Silva. Well-Founded Coalgebras, Revisited. Mathematical Structures in Computer Science (MSCS), 2016.
Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon and Peter Capell. Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. Journal of Aerospace Information Systems (JAIS), 11:702–713, 2014.
- Jean-Baptiste Jeannin and Dexter Kozen. Computing with Capsules. Journal of Automata, Languages and Combinatorics (JALC), 17(2–4):185–204, 2012.
Refereed Conference Publications
- Julie L. Newcomb, Satish Chandra, Jean-Baptiste Jeannin, Cole Schlesinger and Manu Sridharan. IoTa: A Calculus for Internet of Things Automation. In Onward!, part of Systems, Programming, Languages and Applications: Software for Humanity (SPLASH), 2017.
- Yanni Kouskoulas, Daniel Genin, Aurora Schmidt and Jean-Baptiste Jeannin. Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics. In Interactive Theorem Proving (ITP), 2017.
- Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry and George Varghese. Correct by Construction Networks using Stepwise Refinement. In USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2017.
- Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System. In Embedded Software (EMSOFT), 2015. Invited paper.
- Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki and André Platzer. A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015.
- Jean-Baptiste Jeannin and André Platzer. dTL2: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems. In International Conference on Automated Reasoning (IJCAR), 2014.
- Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: Semantic Foundations for Networks. In Principles of Programming Languages (POPL), 2014.
- Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Language Constructs for Non-Well-Founded Computation. In 22nd European Symposium on Programming (ESOP), 2013.
- Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, and Nikhil Swamy. DKAL*: Constructing Executable Specifications of Authorization Protocols. In Engineering Secure Software and Systems (ESSoS), 2013.
- Jean-Baptiste Jeannin and Dexter Kozen. Computing with Capsules. In Descriptional Complexity of Formal Systems (DCFS), 2012. Invited paper.
- Jean-Baptiste Jeannin and Dexter Kozen. Capsules and Separation. In Logic in Computer Science (LICS), 2012.
- Jean-Baptiste Jeannin. Capsules and Closures. In Mathematical Foundations of Programming Semantics (MFPS XXVII), 2011.
- Heber Herencia-Zapana, Jean-Baptiste Jeannin, and César Muñoz. Formal Verification of Safety Buffers for State-Based Conflict Detection and Resolution. In 27th International Congress of the Aeronautical Sciences (ICAS), 2010.