Kristin-Yvonne Rozier

Interest Areas

• Formal methods, verification and validation of safety-critical systems.
• Design-time checking of system logic and system requirements with applications in aerospace systems, automated control, biomedical privacy, secure protocols.
• System and safety health management for intelligent, autonomous Unmanned Aerial Systems.
• Model checking, property-based design, model-based design.
• Linear Temporal Logic satisflability checking, specification debugging techniques and theory.
• Automated reasoning, runtime monitoring, fault tolerance and safety analysis.

Publications

1. Gokul Hariharan, Brian Kempa, Tichakorn Wongpiromsarn, Phillip H. Jones, and Kristin Y. Rozier. “MLTL Multi-type (MLTLM): A Logic for Reasoning about Signals of Different Types.” In Proceedings of the 15th International Workshop on Numerical Software Verification (NSV), a workshop of FLoC. Springer, Haifa, Israel, August 11, 2022. PDF BibTeX Website
2. Orion Staskal, Josh Simac, Logan Swayne, and Kristin Yvonne Rozier. “Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas.” In Proceedings of SESS 2022: Software Engineering for Smart Systems, a workshop of IEEE COMPSAC: Computers, Software & Applications in an Uncertain World. IEEE, Virtual, June 27-July 1, 2022. PDF BibTeX Website
3. Brian Kempa, Chris Johannsen, Kristin Yvonne Rozier. “Improving Usability and Trust in Real-Time Verification of a Large-Scale Complex Safety-Critical System.” In Ada User Journal, Work in Progress (WiP) track, 2022. PDF BibTeX Slides
4. Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier. “Satisfiability Checking for Mission-time LTL.” In Information and Computation Journal, Elsevier, volume 104923, ISSN 0890-5401, May, 2022. DOI https://doi.org/10.1016/j.ic.2022.104923.104923. PDF ScienceDirect Link BibTeX
5. Alexis Aurandt, Phillip Jones, and Kristin Yvonne Rozier. “Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I.” In Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022), Caltech, California, USA, May 24-27, 2022. PDF BibTeX Website
6. Zachary Luppen, Michael Jacks, Nathan Baughman, Benjamin Hertz, James Cutler, Dae Young Lee, and Kristin Yvonne Rozier. “Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry.” In Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022), Caltech, California, USA, May 24-27, 2022. PDF BibTeX Website
7. Rohit Dureja and Kristin Yvonne Rozier. “Incremental Design-space Model Checking Via Reusable Reachable State Approximations” In Formal Methods in System Design (FMSD) Journal, Springer, 2022. DOI: https://doi.org/10.1007/s10703-022-00389-5 PDF SpringerLink BibTeX
8. Abigail Hammer, Matthew Cauwels, Benjamin Hertz, Phillip Jones, and Kristin Yvonne Rozier. “Integrating Runtime Verification into an Automated UAS Traffic Management System.” In Innovations in Systems and Software Engineering: A NASA Journal, Springer, July, 2021. DOI: https://doi.org/10.1007/s11334-021-00407-5 BibTeX
9. Christopher Johannsen, Marcella Anderson, William Burken, Ellie Diersen, John Edgren, Colton Glick, Stephanie Jou, Adhyaksh Kumar, John Levandowski, Evelyn Moyer, Taylor Roquet, Alexander VandeLoo, and Kristin Yvonne Rozier. “OpenUAS Version 1.0.” In Proceedings of the 2021 IEEE International Conference on Unmanned Aircraft Systems (ICUAS), IEEE, Athens, Greece (Virtual), June 15-18, 2021. PDF BibTeX Website Video
10. Benjamin Hertz, Zachary Luppen and Kristin Yvonne Rozier. “Integrating Runtime Verification into a Sounding Rocket Control System.” In Proceedings of the 13th NASA Formal Methods Symposium (NFM 2021), Springer, Virtual, May 24-28, 2021. PDF  SpringerLink  BibTeX  Website  Video
11. Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier, Holger Schlingloff, Michael Winikoff, and Neil Yorke-Smith. “Towards a Framework for Certification of Reliable Autonomous Systems.” In 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS) Journal-first (JAAMAS) track, Springer, London, UK (Virtual), May 3-7, 2021. PDF SpringerLink BibTeX
12. Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier, Holger Schlingloff, Michael Winikoff, and Neil Yorke-Smith. “Towards a Framework for Certification of Reliable Autonomous Systems.” In Journal of Autonomous Agents and Multi-Agent Systems (JAAMAS), volume 35, number 8, Springer, January, 2021. DOI: https://doi.org/10.1007/s10458-020-09487-2 PDF SpringerLink BibTeX
13. Jianwen Li, Yueling Zhang, Geguang Pu, Kristin Y. Rozier, and Moshe Y. Vardi. “SAT-based Explicit LTLf Satisfiability Checking.” In Artificial Intelligence Journal, Elsevier, 2020. PDF BibTeX
14. Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, and Kristin Yvonne Rozier. “Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration.” In Proceedings of the Twentieth International Conference on Formal Methods in Computer-Aided Design (FMCAD), IEEE, September 21-24, 2020. BibTeX  Website  EasyChair-SmartSlides  Short Video  Long Video
15. Matthew Cauwels, Abigail Hammer, Benjamin Hertz, Phillip Jones, and Kristin Yvonne Rozier. “Integrating Runtime Verification into an Automated UAS Traffic Management System.” In Proceedings of DETECT: international workshop on moDeling, vErification and Testing of dEpendable CriTical systems, volume 1269 of Communications in Computer and Information Science (CCIS),pages 340{357, Springer, L’Aquila, Italy, September 14-18, 2020. DOI: https://doi.org/10.1007/978-3-030-59155-7 26 PDF BibTeX Website Video Presentation
16. Brian Kempa, Pei Zhang, Phillip Jones, Joseph Zambreno, and Kristin Yvonne Rozier. “Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2.” In Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), volume 12288 of Lecture Notes in Computer Science (LNCS), pages 196-214, Springer-Verlag, Vienna, Austria, September 1-3, 2020. DOI: 10.1007/978-3-030-57628-8_12 PDF BibTeX Website
17. Rohit Dureja, and Kristin Yvonne Rozier. “Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks.” Journal of Aerospace Information Systems (JAIS), volume 17, number 7, pages 322-335, AIAA, 2020. DOI:10.2514/1.I010769. PDF BibTeX
18. Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman and Kristin Yvonne Rozier. “Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties.” In Formal Methods in Computer-Aided Design (FMCAD), IEEE/ACM, San Jose, California, USA, October 22-25, 2019. DOI:10.23919/FMCAD.2019 .8894265. PDF  EasyChair-Preprint  BibTeX  Website
19. Kristin Yvonne Rozier. “On Teaching Applied Formal Methods in Aerospace Engineering.” In Proceedings of the Formal Methods Teaching Workshop (FMTea) at the 3rd World Congress on Formal Methods, Springer Lecture Notes in Computer Science (LNCS), Porto, Portugal, October 7, 2019. PDF (Springer Link PDF) BibTeX EasyChair-SmartSlides
20. Jianwen Li, Moshe Vardi, and Kristin Yvonne Rozier. “Satisfiability Checking for Mission-Time LTL.”In Proceedings of the 31st International Conference on Computer Aided Verification (CAV), Springer-Verlag, New York, New York, USA, July 15-18, 2019. PDF (Springer Link) BibTeX Slides
21. Rohit Dureja, Jianwen Li, Geguang Pu, Kristin Yvonne Rozier and Moshe Vardi. “Intersection and Rotation of Assumption Literals Boosts Bug-Finding.” In Proceedings of the 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), volume 12031 of Lecture Notes in Computer Science (LNCS), pages 180-192, Springer-Verlag, New York, New York, USA, July 13–14, 2019. PDF (Springer Link) BibTeX Website
22. Kristin Yvonne Rozier. “From Simulation to Runtime Verification and Back: Connecting Single-Run Verification Techniques.” In 2019 Spring Simulation Conference (SpringSim’19). Tucson, Arizona, April 29 – May 2, 2019. PDF BibTeX
23. Jianwen Li, Yueling Zhang, Geguang Pu, Kristin Y. Rozier, and Moshe Y. Vardi. “SAT-based Explicit LTLf Satisfiability Checking.” In Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19). Honolulu, Hawaii, January 27 – February 1, 2019. PDF BibTeX
24. Jianwen Li and Kristin Yvonne Rozier. “MLTL Benchmark Generation via Formula Progression.” In Proceedings of the 18th International Conference on Runtime Verification (RV18), Springer-Verlag, Limassol, Cyprus, November 10-13, 2018. PDF BibTeX
25. Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, and Moshe Vardi. “SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability.” In Proceedings of the 30th International Conference on Computer Aided Verification (CAV), Springer-Verlag, Oxford, UK, 2018. PDF  BibTeX  Website&Models  EasyChair-SmartSlides
26. Rohit Dureja and Kristin Yvonne Rozier. “More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D3).” In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), part I, volume 10805 of Lecture Notes in Computer Science (LNCS), pages 309-327, Springer-Verlag, Thessaloniki, Greece, 14-21 April 2018. (Received the “Artifact Evaluated Stamp” — highest mark from Artifact Evaluation Review Committee) PDF  BibTeX  Additional Proofs/Results Website  Benchmarks/Code/Datasets