Capsules and Closures. - Jean-Baptiste Jeannin (MFPS, 2011)

Capsules and Closures: A Small-Step Approach. - Jean-Baptiste Jeannin (Logic and Program Semantics, 2012)

Capsules and Separation. - Jean-Baptiste Jeannin; Dexter Kozen (LICS, 2012)

Computing with Capsules. - Jean-Baptiste Jeannin; Dexter Kozen (J. Autom. Lang. Comb., 2012)

Language Constructs for Non-Well-Founded Computation. - Jean-Baptiste Jeannin; Dexter Kozen; Alexandra Silva 001 (ESOP, 2013)

dkal ⋆ : Constructing Executable Specifications of Authorization Protocols. - Jean-Baptiste Jeannin; Guido de Caso; Juan Chen 002; Yuri Gurevich; Prasad Naldurg; Nikhil Swamy (ESSoS, 2013)

Capsules and Non-Well-Founded Computation. - Jean-Baptiste Jeannin (2013)

dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. - Jean-Baptiste Jeannin; André Platzer (IJCAR, 2014)

NetkAT: semantic foundations for networks. - Carolyn Jane Anderson; Nate Foster; Arjun Guha; Jean-Baptiste Jeannin; Dexter Kozen; Cole Schlesinger; David Walker 001 (POPL, 2014)

Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. - Khalil Ghorbal; Jean-Baptiste Jeannin; Erik Zawadzki; André Platzer; Geoffrey J. Gordon; Peter Capell (J. Aerosp. Inf. Syst., 2014)

Formal verification of ACAS X, an industrial airborne collision avoidance system. - Jean-Baptiste Jeannin; Khalil Ghorbal; Yanni Kouskoulas; Ryan W. Gardner; Aurora C. Schmidt; Erik Zawadzki; André Platzer (EMSOFT, 2015)

A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. - Jean-Baptiste Jeannin; Khalil Ghorbal; Yanni Kouskoulas; Ryan W. Gardner; Aurora C. Schmidt; Erik Zawadzki; André Platzer (TACAS, 2015)

Type inference for static compilation of JavaScript. - Satish Chandra 001; Colin S. Gordon; Jean-Baptiste Jeannin; Cole Schlesinger; Manu Sridharan; Frank Tip; Young-Il Choi (OOPSLA, 2016)

Type Inference for Static Compilation of JavaScript (Extended Version). - Satish Chandra 001; Colin S. Gordon; Jean-Baptiste Jeannin; Cole Schlesinger; Manu Sridharan; Frank Tip; Young-Il Choi (CoRR, 2016)

Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. - Andrei Marian Dan; Manu Sridharan; Satish Chandra 001; Jean-Baptiste Jeannin; Martin T. Vechev (CAV (2), 2017)

Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics. - Yanni Kouskoulas; Daniel Genin; Aurora C. Schmidt; Jean-Baptiste Jeannin (ITP, 2017)

Correct by Construction Networks Using Stepwise Refinement. - Leonid Ryzhyk; Nikolaj S. Bjørner; Marco Canini; Jean-Baptiste Jeannin; Cole Schlesinger; Douglas B. Terry; George Varghese (NSDI, 2017)

I¿¿¿: a calculus for internet of things automation. - Julie L. Newcomb; Satish Chandra 001; Jean-Baptiste Jeannin; Cole Schlesinger; Manu Sridharan (Onward!, 2017)

Fission: Secure Dynamic Code-Splitting for JavaScript. - Arjun Guha; Jean-Baptiste Jeannin; Rachit Nigam; Jane Tangen; Rian Shambaugh (SNAPL, 2017)

CoCaml: Functional Programming with Regular Coinductive Types. - Jean-Baptiste Jeannin; Dexter Kozen; Alexandra Silva 001 (Fundam. Informaticae, 2017)

Well-founded coalgebras, revisited. - Jean-Baptiste Jeannin; Dexter Kozen; Alexandra Silva 001 (Math. Struct. Comput. Sci., 2017)

A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. - Jean-Baptiste Jeannin; Khalil Ghorbal; Yanni Kouskoulas; Aurora C. Schmidt; Ryan W. Gardner; Stefan Mitsch; André Platzer (Int. J. Softw. Tools Technol. Transf., 2017)

Formal Specification of Continuum Deformation Coordination. - Hossein Rastgoftar; Jean-Baptiste Jeannin; Ella M. Atkins (ACC, 2019)

Towards Automatic Inference of Inductive Invariants. - Haojun Ma; Aman Goel; Jean-Baptiste Jeannin; Manos Kapritsos; Baris Kasikci; Karem A. Sakallah (HotOS, 2019)

I4: incremental inference of inductive invariants for verification of distributed protocols. - Haojun Ma; Aman Goel; Jean-Baptiste Jeannin; Manos Kapritsos; Baris Kasikci; Karem A. Sakallah (SOSP, 2019)

Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions. - Kyle D. Julian; Shivam Sharma; Jean-Baptiste Jeannin; Mykel J. Kochenderfer (CoRR, 2019)

Formal Verification of Swerving Maneuvers for Car Collision Avoidance. - Aakash Abhishek; Harry Sood; Jean-Baptiste Jeannin (ACC, 2020)

Accelerating Legacy String Kernels via Bounded Automata Learning. - Kevin Angstadt; Jean-Baptiste Jeannin; Westley Weimer (ASPLOS, 2020)

Formal verification of braking while swerving in automobiles. - Aakash Abhishek; Harry Sood; Jean-Baptiste Jeannin (HSCC, 2020)

Grand Challenges for Embedded Security Research in a Connected World. - Wayne P. Burleson; Kevin Fu; Denise L. Anthony; Jorge Guajardo; Carl A. Gunter; Kyle Ingols; Jean-Baptiste Jeannin; Farinaz Koushanfar; Carl E. Landwehr; Susan Squires (CoRR, 2020)

A Physics-Based Finite-State Abstraction for Traffic Congestion Control. - Hossein Rastgoftar; Jean-Baptiste Jeannin (ACC, 2021)

A program logic to verify signal temporal logic specifications of hybrid systems. - Hammad Ahmad; Jean-Baptiste Jeannin (HSCC, 2021)

A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes. - Mohit Tekriwal; Karthik Duraisamy; Jean-Baptiste Jeannin (NFM, 2021)

A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems: Extended Technical Report. - Hammad Ahmad; Jean-Baptiste Jeannin (CoRR, 2021)

Towards Verified Rounding Error Analysis for Stationary Iterative Methods. - Ariel Kellison; Mohit Tekriwal; Jean-Baptiste Jeannin; Geoffrey C. Hulette (Correctness@SC, 2022)

Twine: A Chisel Extension for Component-Level Heterogeneous Design. - Shibo Chen 001; Yonathan Fisseha; Jean-Baptiste Jeannin; Todd M. Austin (DATE, 2022)

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; Konstantinos Mamouras (EMSOFT, 2022)

Automating Geometric Proofs of Collision Avoidance with Active Corners. - Nishant Kheterpal; Elanor Tang; Jean-Baptiste Jeannin (FMCAD, 2022)

Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation. - Jiawei Chen; José Luiz Vargas de Mendonça; Shayan Jalili; Bereket Ayele; Bereket Ngussie Bekele; Zhemin Qu; Pranjal Sharma; Tigist Shiferaw; Yicheng Zhang; Jean-Baptiste Jeannin (FTSCS, 2022)

Dandelion: Certified Approximations of Elementary Functions. - Heiko Becker; Mohit Tekriwal; Eva Darulova; Anastasia Volkova; Jean-Baptiste Jeannin (ITP, 2022)

Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems. - Haojun Ma; Hammad Ahmad; Aman Goel; Eli Goldweber; Jean-Baptiste Jeannin; Manos Kapritsos; Baris Kasikci (USENIX ATC, 2022)

Formal verification of iterative convergence of numerical algorithms. - Mohit Tekriwal; Joshua Miller; Jean-Baptiste Jeannin (CoRR, 2022)

A Concurrent Switching Model for Traffic Congestion Control. - Hossein Rastgoftar; Xun Liu; Jean-Baptiste Jeannin (CoRR, 2022)

Synthesizing Legacy String Code for FPGAs Using Bounded Automata Learning. - Kevin Angstadt; Tommy Tracy II; Kevin Skadron; Jean-Baptiste Jeannin; Westley Weimer (IEEE Micro, 2022)

Efficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes. - Liren Yang; Hang Zhang; Jean-Baptiste Jeannin; Necmiye Ozay (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022)

Security Verification of Low-Trust Architectures. - Qinhan Tan; Yonathan Fisseha; Shibo Chen 001; Lauren Biernacki; Jean-Baptiste Jeannin; Sharad Malik; Todd M. Austin (CCS, 2023)

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; Westley Weimer (ICSE, 2023)

Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. - Mohit Tekriwal; Andrew W. Appel; Ariel E. Kellison; David Bindel; Jean-Baptiste Jeannin (CICM, 2023)

Falsification of a Vision-based Automatic Landing System. - Sara Shoouri; Shayan Jalili; Jiahong Xu; Isabelle Gallagher; Yuhao Zhang; Joshua Wilhelm; Necmiye Ozay; Jean-Baptiste Jeannin (CoRR, 2023)

Formalization of Asymptotic Convergence for Stationary Iterative Methods. - Mohit Tekriwal; Joshua Miller; Jean-Baptiste Jeannin (NFM, 2024)

Formally verified asymptotic consensus in robust networks. - Mohit Tekriwal; Avi Tachna-Fram; Jean-Baptiste Jeannin; Manos Kapritsos; Dimitra Panagou (TACAS (1), 2024)

Synchronous Programming with Refinement Types. - Jiawei Chen; José Luiz Vargas de Mendonça; Bereket Ayele; Bereket Ngussie Bekele; Shayan Jalili; Pranjal Sharma; Nicholas Wohlfeil; Yicheng Zhang; Jean-Baptiste Jeannin (Proc. ACM Program. Lang., 2024)