Jean-Baptiste Jeannin

Publication Activity (10 Years)

Years Active: 2011-2023
Publications (10 Years): 47

Top Topics

Collision Avoidance

Formal Verification

Technical Report

Top Venues

Publications

Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik, Todd M. Austin
Security Verification of Low-Trust Architectures. CCS (2023)
Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik, Todd M. Austin
Security Verification of Low-Trust Architectures. CoRR (2023)
Sara Shoouri, Shayan Jalili, Jiahong Xu, Isabelle Gallagher, Yuhao Zhang, Joshua Wilhelm, Necmiye Ozay, Jean-Baptiste Jeannin
Falsification of a Vision-based Automatic Landing System. CoRR (2023)
Hammad Ahmad, Zachary Karas, Kimberly Diaz, Amir Kamil, Jean-Baptiste Jeannin, Westley Weimer
How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms. ICSE (2023)
Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin
Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. CICM (2023)
Liren Yang, Hang Zhang, Jean-Baptiste Jeannin, Necmiye Ozay
Efficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41 (11) (2022)
Haojun Ma, Hammad Ahmad, Aman Goel, Eli Goldweber, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci
Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems. USENIX Annual Technical Conference (2022)
Kevin Angstadt, Tommy Tracy II, Kevin Skadron, Jean-Baptiste Jeannin, Westley Weimer
Synthesizing Legacy String Code for FPGAs Using Bounded Automata Learning. IEEE Micro 42 (5) (2022)
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
Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation. FTSCS (2022)
Hossein Rastgoftar, Xun Liu, Jean-Baptiste Jeannin
A Concurrent Switching Model for Traffic Congestion Control. CoRR (2022)
Nishant Kheterpal, Elanor Tang, Jean-Baptiste Jeannin
Automating Geometric Proofs of Collision Avoidance with Active Corners. CoRR (2022)
Shibo Chen, Yonathan Fisseha, Jean-Baptiste Jeannin, Todd M. Austin
Twine: A Chisel Extension for Component-Level Heterogeneous Design. DATE (2022)
Liren Yang, Hang Zhang, Jean-Baptiste Jeannin, Necmiye Ozay
Efficient Backward Reachability using the Minkowski Difference of Constrained Zonotopes. CoRR (2022)
Nishant Kheterpal, Elanor Tang, Jean-Baptiste Jeannin
Automating Geometric Proofs of Collision Avoidance with Active Corners. FMCAD (2022)
Mohit Tekriwal, Joshua Miller, Jean-Baptiste Jeannin
Formal verification of iterative convergence of numerical algorithms. CoRR (2022)
Ariel Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, Geoffrey C. Hulette
Towards Verified Rounding Error Analysis for Stationary Iterative Methods. Correctness@SC (2022)
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin
Dandelion: Certified Approximations of Elementary Functions. ITP (2022)
Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou
Formally verified asymptotic consensus in robust networks. CoRR (2022)
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin
Dandelion: Certified Approximations of Elementary Functions. CoRR (2022)
Jean-Baptiste Jeannin, Jiawei Chen, José Luiz Vargas de Mendonça, Konstantinos Mamouras
Work-in-Progress: Towards a Theory of Robust Quantitative Semantics for Signal Temporal Logic. EMSOFT (2022)
Hammad Ahmad, Jean-Baptiste Jeannin
A program logic to verify signal temporal logic specifications of hybrid systems. HSCC (2021)
Mohit Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin
A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes. NFM (2021)
Hossein Rastgoftar, Jean-Baptiste Jeannin
A Physics-Based Finite-State Abstraction for Traffic Congestion Control. CoRR (2021)
Hossein Rastgoftar, Jean-Baptiste Jeannin
A Physics-Based Finite-State Abstraction for Traffic Congestion Control. ACC (2021)
Mohit Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin
A formal proof of the Lax equivalence theorem for finite difference schemes. CoRR (2021)
Hammad Ahmad, Jean-Baptiste Jeannin
A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems: Extended Technical Report. CoRR (2021)
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
Grand Challenges for Embedded Security Research in a Connected World. CoRR (2020)
Aakash Abhishek, Harry Sood, Jean-Baptiste Jeannin
Formal verification of braking while swerving in automobiles. HSCC (2020)
Kevin Angstadt, Jean-Baptiste Jeannin, Westley Weimer
Accelerating Legacy String Kernels via Bounded Automata Learning. ASPLOS (2020)
Aakash Abhishek, Harry Sood, Jean-Baptiste Jeannin
Formal Verification of Swerving Maneuvers for Car Collision Avoidance. ACC (2020)
Hossein Rastgoftar, Jean-Baptiste Jeannin, Ella M. Atkins
Formal Specification of Continuum Deformation Coordination. CoRR (2019)
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah
Towards Automatic Inference of Inductive Invariants. HotOS (2019)
Kyle D. Julian, Shivam Sharma, Jean-Baptiste Jeannin, Mykel J. Kochenderfer
Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions. CoRR (2019)
Hossein Rastgoftar, Jean-Baptiste Jeannin, Ella M. Atkins
Formal Specification of Continuum Deformation Coordination. ACC (2019)
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah
I4: incremental inference of inductive invariants for verification of distributed protocols. SOSP (2019)
Arjun Guha, Jean-Baptiste Jeannin, Rachit Nigam, Jane Tangen, Rian Shambaugh
Fission: Secure Dynamic Code-Splitting for JavaScript. SNAPL (2017)
Andrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin T. Vechev
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. CAV (2) (2017)
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora C. Schmidt, Ryan W. Gardner, Stefan Mitsch, André Platzer
A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. Int. J. Softw. Tools Technol. Transf. 19 (6) (2017)
Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, George Varghese
Correct by Construction Networks Using Stepwise Refinement. NSDI (2017)
Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva
Well-founded coalgebras, revisited. Math. Struct. Comput. Sci. 27 (7) (2017)
Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva
CoCaml: Functional Programming with Regular Coinductive Types. Fundam. Informaticae 150 (3-4) (2017)
Yanni Kouskoulas, Daniel Genin, Aurora C. Schmidt, Jean-Baptiste Jeannin
Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics. ITP (2017)
Julie L. Newcomb, Satish Chandra, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan
I¿¿¿: a calculus for internet of things automation. Onward! (2017)
Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, Young-Il Choi
Type Inference for Static Compilation of JavaScript (Extended Version). CoRR (2016)
Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin, Cole Schlesinger, Manu Sridharan, Frank Tip, Young-Il Choi
Type inference for static compilation of JavaScript. OOPSLA (2016)
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, André Platzer
Formal verification of ACAS X, an industrial airborne collision avoidance system. EMSOFT (2015)
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, André Platzer
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. TACAS (2015)
Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, David Walker
NetkAT: semantic foundations for networks. POPL (2014)
Jean-Baptiste Jeannin, André Platzer
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. IJCAR (2014)
Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, Peter Capell
Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. J. Aerosp. Inf. Syst. 11 (10) (2014)
Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
dkal ⋆ : Constructing Executable Specifications of Authorization Protocols. ESSoS (2013)
Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva
Language Constructs for Non-Well-Founded Computation. ESOP (2013)
Jean-Baptiste Jeannin, Dexter Kozen
Computing with Capsules. J. Autom. Lang. Comb. 17 (2-4) (2012)
Jean-Baptiste Jeannin, Dexter Kozen
Computing with Capsules. DCFS (2012)
Jean-Baptiste Jeannin
Capsules and Closures: A Small-Step Approach. Logic and Program Semantics (2012)
Jean-Baptiste Jeannin, Dexter Kozen
Capsules and Separation. LICS (2012)
Jean-Baptiste Jeannin
Capsules and Closures. MFPS (2011)