Education:

• Ph.D. Computer Science, Cornell University, 2013
• M.Eng. Computer Science, Cornell University, 2008
• Diplôme d’Ingénieur, École Polytechnique, France, 2007

Teaching: ^top

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

Biography: ^top

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.

Before coming to Michigan, Jean-Baptiste was working on Javascript compilers and software security, as a Researcher at Samsung Research America in Mountain View, California. He also led the formal analysis of the Next-Generation Airborne Collision Avoidance System (ACAS X), as a Post Doctoral Fellow working with André Platzer in the Logical Systems Lab at Carnegie Mellon University, and in collaboration with the Johns Hopkins Applied Physics Laboratory. He received a Ph.D. in Computer Science from Cornell University in 2013, where he was advised by Dexter Kozen. He also received a Master of Engineering in Computer Science from Cornell University in 2008, and a Diplôme d’Ingénieur from École Polytechnique, France in 2007. In his spare time, he likes to fly small airplanes.

Positions Held at UM

Assistant Professor, Aerospace Engineering, 2017 to present

Awards: ^top

Honors and Awards

Acheson Award 2007, full tuition fellowship at Cornell University

Society Memberships

Member of the Association for Computing Machinery (ACM)

Publications: ^top

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.
• Arjun Guha, Jean-Baptiste Jeannin, Rachit Nigam, Rian Shambaugh and Jane Tangen. Fission: Dynamic Code Splitting for Javascript. In Summit on Advances in Programming Languages (SNAPL), 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.
• Satish Chandra, Colin Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridha- ran, Frank Tip and Young-il Choi. Type Inference for Static Compilation of JavaScript. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2016.
• 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.