- LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs. Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, David Bindel. In 30th IEEE International Symposium on Computer Arithmetic, 2023.
- Security Verification of Low-Trust Architectures. Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik and Todd Austin. ACM Conference on Computer and Communications Security (CCS 2023). [full text (.pdf)]
- Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. Mohit K. Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin. In 16th Conference on Intelligent Computer Mathematics, 2023.
- A Concurrent Switching Model for Traffic Congestion Control. Hossein Rastgofta, Xun Liu and Jean-Baptiste Jeannin. In Modeling, Estimation and Control Conference (MECC 2023). [full text (.pdf)]
- Towards a Study of Performance for Safe Neural Network Training. Nishant Kheterpal and Jean-Baptiste Jeannin. In 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS 2023). [full text (.pdf)]
- 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, and Westley Weimer. In International Conference on Software Engineering (ICSE 2023). [full text (.pdf)]
- 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)] [video]
- 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] [video]
- 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)]
