| 2025 | CAV | Infinite-State Liveness Checking with rlive. | Alessandro Cimatti, Alberto Griggio, Christopher Johannsen, Kristin Yvonne Rozier, Stefano Tonetta |
| 2025 | FMCAD | R2U2 Playground: Visualization of a Real-time, Temporal Logic Runtime Monitor. | Alexis A. Aurandt, Kristin Yvonne Rozier, Phillip H. Jones |
| 2025 | FMCAD | Scalable MLTL Runtime Monitoring and Satisfiability via Bit-Vector Encoding. | Christopher Johannsen, Phillip H. Jones, Kristin Yvonne Rozier, Tichakorn Wongpiromsarn |
| 2025 | TACAS | Formally Verifying a Transformation from MLTL Formulas to Regular Expressions. | Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier |
| 2024 | CAV | The MoXI Model Exchange Tool Suite. | Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier |
| 2024 | FMICS | Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical Systems. | Alexis A. Aurandt, Phillip H. Jones, Kristin Yvonne Rozier, Tichakorn Wongpiromsarn |
| 2023 | CAV | R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software. | Chris Johannsen, Phillip H. Jones, Brian Kempa, Kristin Yvonne Rozier, Pei Zhang |
| 2023 | IFM | Mission-Time LTL (MLTL) Formula Validation via Regular Expressions. | Jenna Elwing, Laura P. Gamboa Guzman, Jeremy Sorkin, Chiara Travesset, Zili Wang, Kristin Yvonne Rozier |
| 2023 | VISSOFT | What's in a Name? Linear Temporal Logic Literally Represents Time Lines. | Runming Li, Keerthana Gurushankar, Marijn J. H. Heule, Kristin Yvonne Rozier |
| 2018 | CAV | SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability. | Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi |
| 2018 | ISoLA | A Broader View on Verification: From Static to Runtime and Back (Track Summary). | Wolfgang Ahrendt, Marieke Huisman, Giles Reger, Kristin Yvonne Rozier |
| 2018 | TACAS | More Scalable LTL Model Checking via Discovering Design-Space Dependencies ( D^3 D 3 ). | Rohit Dureja, Kristin Yvonne Rozier |
| 2017 | FMCAD | FuseIC3: An algorithm for checking large design spaces. | Rohit Dureja, Kristin Yvonne Rozier |
| 2017 | RV | On the Evaluation and Comparison of Runtime Verification Tools for Hardware and Cyber-Physical Systems. | Kristin Yvonne Rozier |
| 2017 | RV | R2U2: Tool Overview. | Kristin Yvonne Rozier, Johann Schumann |
| 2016 | CAV | Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. | Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier |
| 2014 | TACAS | Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems. | Thomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann |