- 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)] [slides]
- 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)] [slides] [video]
- 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. Shibo Chen, Yonathan Fisseha, Jean-Baptiste Jeannin and Todd AustiHeiko 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 Abstraction 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)]
