Publications

Publications (Peer-Reviewed)

  1. Zili Wang, Laura P. Gamboa Guzman, Kristin Y. Rozier. WEST: Interactive Validation of Mission-time Linear Temporal Logic (MLTL), to appear in Science of Computer Programming, 2025. PDF Website
  2. Alec Rosentrater, Zili Wang, Katherine Kosaian and Kristin Yvonne Rozier. “Language Partitioning for Mission-time Linear Temporal Logic.” In Proceedings of the 17th NASA Formal Methods Symposium (NFM 2025), volume TBD of Lecture Notes in Computer Science (LNCS), Springer, Williamsburg, Virginia, USA, June 11-13, 2025. PDF
  3. Alexis Aurandt, Phillip Jones and Kristin Yvonne Rozier. “Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust.” In Proceedings of the 17th NASA Formal Methods Symposium (NFM 2025), volume TBD of Lecture Notes in Computer Science (LNCS), Springer, Williamsburg, Virginia, USA, June 11-13, 2025. PDF Website
  4. Zili Wang, Katherine Kosaian, and Kristin Yvonne Rozier. “Formally Verifying a Transformation from MLTL Formulas to Regular Expressions.” In 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume TBD of Lecture Notes in Computer Science (LNCS), pages TBD, Springer-Verlag, Hamilton, Canada, May 3–8, 2025. PDF Website
  5. Gokul Hariharan, Brian Kempa, Tichakorn Wongpiromsarn, Phillip H. Jones, and Kristin Y. Rozier. “MLTL Multi-type: A Typed Logic for Cyber-Physical Systems.” In Transactions on Embedded Computing Systems, 2024.
  6. Rohit Dureja, Jason Baumgartner, Raj Kumar Gajavelly, Robert Kanzelman, and Kristin Yvonne Rozier. “Toward Exhaustive Sequential Redundancy Removal.” In Proceedings of the Twenty-fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD), IEEE, October 14–18, 2024.
  7. Maurice H. ter Beek, Rod Chapman, Rance Cleaveland, Hubert Garavel, Rong Gu, Ivo ter Horst, Jeroen J. A. Keiren, Thierry Lecomte, Michael Leuschel, Kristin Y. Rozier, Augusto Sampaio, Cristina Seceleanu, Martyn Thomas, Tim A. C. Willemse, Lijun Zhang. ”Formal Methods in Industry.” In Formal Aspects of Computing Journal, August, 2024. DOI: 10.1145/3689374
  8. Alexis Aurandt, Phillip H. Jones, Kristin Yvonne Rozier and Tichakorn Wongpiromsarn. “Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical Systems.” In Proceedings of the 29th International Conference on Formal Methods for Industrial Critical Systems (FMICS), LNCS, Springer, Milan, Italy, September 9–11, 2024. DOI: 10.1007/ 978-3-031-68150-9 13 Print ISBN: 978-3-031-68149-3 PDF Website
  9. Katherine Kosaian, Yong Kiam Tan, and Kristin Yvonne Rozier. “Formalizing Coppersmith’s Method in Isabelle/HOL.” In Proceedings of the 17th Conference on Intelligent Computer Mathematics (CICM), LNCS, Springer, Montr´eal, Qu´ebec, Canada, August 5–9, 2024.
  10. C. Johannsen, K. Nukala∗ , R. Dureja, A. Irfan, N. Shankar, C. Tinelli, M. Y. Vardi, and K. Y. Rozier. “The MoXI Model Exchange Tool Suite.” In Proceedings of 36th International Conference on Computer Aided Verification (CAV). volume 14681, LNCS, Springer, July, 2024.
  11. K. Y. Rozier, R. Dureja, A. Irfan, C. Johannsen, K. Nukala , N. Shankar, C. Tinelli, and M. Y. Vardi. “MoXI: An Intermediate Language for Symbolic Model Checking.” In: Proceedings of the 30th International Symposium on Model Checking Software (SPIN). LNCS, Springer, April, 2024.
  12. Jenna Elwing, Laura Gamboa-Guzman, Jeremy Sorkin, Chiara Travesset, Zili Wang, and Kristin Yvonne Rozier. “Mission-Time LTL (MLTL) Formula Validation via Regular Expressions.” In Proceedings of the 18th International Conference on integrated Formal Methods (iFM), Springer, Leiden, The Netherlands, November 13-15, 2023. DOI: 10.1007/978-3-031-47705-8_15 PDF SpringerNature BibTeX Website Slides
  13. Runming Li, Keerthana Gurushankar, Marijn J.H. Heule, and Kristin Y.Rozier. “What’s in a Name? Linear Temporal Logic Literally Represents Time Lines.” In Proceedings of the 11th IEEE Working Conference on Software Visualization (VISSOFT 2023), Botota, Columbia, October 1–2, 2023. DOI: 10.1109/VISSOFT60811.2023.00018 IEEEXplore BibTeX Slides
  14. Chris Johannsen, Brian Kempa, Phillip Jones, Kristin Yvonne Rozier and Tichakorn Wongpiromsarn. “Impossible Made Possible: Encoding Intractable Specifications via Implied Domain Constraints.” In Proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems (FMICS), Springer, Antwerp, Belgium, September 20-22, 2023. DOI: 10.1007/978-3-031-43681-9_9 PDF SpringerNature BibTeX Website Slides
  15. Pei Zhang, Alexis Aurandt, Rohit Dureja, Phillip Jones, and Kristin Y. Rozier. “Model Predictive Runtime Verification for Cyber-Physical Systems with Real-Time Deadlines.” In Proceedings of the 21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Springer, Antwerp, Belgium, September 19–21, 2023. DOI: 10.1007/978-3-031-42626-1_10 PDF SpringerNature Slides
  16. Gokul Hariharan, Phillip H. Jones, Kristin Y. Rozier, and Tichakorn Wongpiromsarn. “Maximum Satisfiability in Mission-time Linear Temporal Logic.” In Proceedings of the 21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Springer, Antwerp, Belgium, September 19–21, 2023. DOI: 10.1007/978-3-031-42626-1_6 PDF SpringerNature Website
  17. Chris Johannsen, Phillip Jones, Brian Kempa, Kristin Yvonne Rozier, and Pei Zhang. “R2U2 Version 3.0: Re-imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software.” In Proceedings of the 35th International Conference on Computer Aided Verification (CAV), Springer-Verlag, Paris, France, July 17-22, 2023. DOI: 10.1007/978-3-031-37709-9_23 PDF SpringerNature BibTeX Website Slides
  18. Laura P. Gamboa Guzmán, and Kristin Yvonne Rozier. “Stalnaker’s Epistemic Logic in Isabelle/HOL.” In Proceedings of the 18th Logical and Semantic Frameworks with Applications (LSFA), Springer, Rome, Italy, July 1–2, 2023. PDF
  19. 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. DOI: 10.1007/978-3-031-21222-2_11 PDF SpringerNature BibTeX Website Slides
  20. 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. DOI: 10.1109/COMPSAC54236.2022.00260 PDF IEEEXplore BibTeX Website
  21. 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, September, 2022. PDF BibTeX Slides
  22. 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: 10.1016/j.ic.2022.104923. PDF ScienceDirect BibTeX
  23. 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. DOI: 10.1007/978-3-031-06773-0_45 PDF SpringerNature BibTeX Website Video
  24. 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. DOI: 10.1007/978-3-031-06773-0_28 PDF SpringerNature BibTeX Website
  25. 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: 10.1007/s10703-022-00389-5 PDF SpringerNature BibTeX
  26. 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: 10.1007/s11334-021-00407-5 SpringerNature BibTeX
  27. 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. DOI: 10.1109/ICUAS51884.2021.9476814 PDF IEEEXplore BibTeX Website Video
  28. 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. DOI: 10.1007/978-3-030-76384-8_10 PDF SpringerNature  BibTeX Website Video
  29. 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. DOI: 10.1007/s10458-020-09487-2 PDF SpringerNature BibTeX
  30. 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. DOI: 10.1016/j.artint.2020.103369 PDF ScienceDirect BibTeX
  31. 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. DOI: 10.34727/2020/isbn.978-3-85448-042-6_8 PDF IEEEXplore BibTeX Website Slides Short Video Long Video
  32. 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: 10.1007/978-3-030-59155-7_26 PDF SpringerNature BibTeX Website Video
  33. 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 SpringerNature BibTeX Website Video
  34. Rohit Dureja, and Kristin Yvonne Rozier. “Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks.” In Journal of Aerospace Information Systems (JAIS), volume 17, number 7, pages 322-335, AIAA, 2020. DOI:10.2514/1.I010769 PDF BibTeX
  35. 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 IEEEXplore BibTeX Website
  36. 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. DOI: 10.1007/978-3-030-32441-4_8 PDF SpringerNature BibTeX Slides
  37. 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. DOI: 10.1007/978-3-030-25543-5_1 PDF SpringerNature BibTeX Slides
  38. 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. DOI: 10.1007/978-3-030-41600-3_12 PDF SpringerNature BibTeX Website
  39. 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. DOI: 10.23919/SpringSim.2019.8732915 PDF IEEEXplore BibTeX
  40. 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. DOI: 10.1016/j.artint.2020.103369 PDF ScienceDirect BibTeX
  41. 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. DOI: 10.1007/978-3-030-03769-7_25 PDF SpringerNature BibTeX
  42. 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. DOI: 10.1007/978-3-319-96142-2_5 PDF SpringerNature BibTeX Website Slides
  43. 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. DOI: 10.1007/978-3-319-89960-2_17 PDF SpringerNature BibTeX Website
  44. Rohit Dureja and Kristin Yvonne Rozier. “FuseIC3: An Algorithm for Checking Large Design Spaces.” In Formal Methods in Computer-Aided Design (FMCAD), IEEE/ACM, Vienna, Austria, October 2-6, 2017. DOI: 10.23919/FMCAD.2017.8102255 PDF IEEEXplore BibTeX Website
  45. Kristin Yvonne Rozier. “On the Evaluation and Comparison of Runtime Verification Tools for Hardware and Cyber-Physical Systems.” In International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), held in conjunction with the 17th International Conference on Runtime Verification (RV), Kalpa Publications, Seattle, Washington, USA, September 13-16, 2017. DOI: 10.29007/pld3 PDF BibTeX
  46. Kristin Yvonne Rozier, and Johann Schumann. “R2U2: Tool Overview.” In International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), held in conjunction with the 17th International Conference on Runtime Verification (RV), Kalpa Publications, Seattle, Washington, USA, September 13-16, 2017. DOI: 10.29007/5pch PDF BibTeX
  47. Patrick Moosbrugger, Kristin Y. Rozier, and Johann Schumann. “R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems.” In Formal Methods in System Design Journal (FMSD), pages 1–31, Springer-Verlag, April, 2017. DOI: 10.1007/s10703-017-0275-x. PDF SpringerNature BibTeX
  48. Eric W.D. Rozier, Kristin Yvonne Rozier, and Ulya Bayram. “Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains.” In Leibniz Transactions on Embedded Systems (LITES) Special Issue on Quantitative Evaluation of Systems (QEST), volume 4, issue 1, article number 5, pg. 05:1-5:26, February, 2017. DOI: 10.4230/LITES-v004-i001-a005. PDF SpringerNature BibTeX
  49. Johann Schumann, Patrick Moosbrugger, and Kristin Y. Rozier. “Runtime Analysis with R2U2: A Tool Exhibition Report.” In Proceedings of the 16th International Conference on Runtime Verification (RV16), Springer-Verlag, Madrid, Spain, September, 2016. DOI: 10.1007/978-3-319-46982-9_35 PDF SpringerNature BibTeX Website Video
  50. Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, and Kristin Yvonne Rozier. “Model Checking at Scale: Automated Air Traffic Control Design Space Exploration.” In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), Springer-Verlag, Toronto, Ontario, Canada, 2016. DOI: 10.1007/978-3-319-41540-6_1 PDF SpringerNature BibTeX Website
  51. Kristin Yvonne Rozier. “Specification: The Biggest Bottleneck in Formal Methods and Autonomy.” In Proceedings of the 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), volume 9971 of Lecture Notes in Computer Science (LNCS), pages 1–19, Springer-Verlag, Toronto, Canada, July 17–18, 2016. (Invited) DOI: 10.1007/978-3-319-48869-1_2 PDF SpringerNature BibTeX
  52. Eric W.D. Rozier and Kristin Yvonne Rozier. “Cascading Solution of Data Dependency Constraints in Z3.” In International Symposium on Artificial Intelligence and Mathematics (ISAIM), AAAI, Ft. Lauderdale, Florida, January 4–6, 2016. (Invited) PDF BibTeX
  53. Eric W.D. Rozier and Kristin Yvonne Rozier. “SMT-Driven Intelligent Storage for Big Data.’” In Proceedings of the Ninth International Workshop on Constraints in Formal Verification (CFV), IEEE, Austin, Texas, USA, November 5, 2015. (Invited) PDF BibTeX
  54. Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta and Kristin Y. Rozier.“Comparing Different Functional Allocations in Automated Air Traffic Control Design.” In Formal Methods in Computer-Aided Design (FMCAD 2015), IEEE/ACM, Austin, Texas, USA, September 27-30, 2015. DOI: 10.1109/FMCAD.2015.7542260 PDF IEEEXplore BibTeX Slides
  55. Johann Schumann, Patrick Moosbrugger, and Kristin Y. Rozier. “R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems.” In Proceedings of the 15th International Conference on Runtime Verification (RV15), Springer-Verlag, Vienna, Austria, September 22–25, 2015. DOI: 10.1007/978-3-319-23820-3_15 PDF SpringerNature BibTeX
  56. Ulya Bayram, Kristin Yvonne Rozier, and Eric W. D. Rozier. “Characterizing Data Dependence Constraints for Dynamic Reliability Using N-Queens Attack Domains.” In Proceedings of the 12th International Conference on Quantitative Evaluation of SysTems (QEST 2015), Madrid, Spain, September 1–3, 2015. DOI: 10.1007/978-3-319-22264-6_14 PDF SpringerNature BibTeX
  57. Johann Schumann, Kristin Y. Rozier, Thomas Reinbacher, Ole J. Mengshoel, Timmy Mbaya, and Corey Ippolito. “Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems.” In International Journal of Prognostics and Health Management (IJPHM), volume 6, number 1, pages 1–27, PHM Society, June, 2015. DOI: 10.36001/ijphm.2015.v6i1.2243 PDF PHMSociety BibTeX
  58. Zhao, Yang, and Rozier, Kristin Yvonne. “Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System.” In Science of Computer Programming Journal, volume 96, number 3, pages 337-353, Elsevier, December, 2014. DOI: 10.1016/j.scico.2014.04.002 PDF ScienceDirect BibTeX Website
  59. Zhao, Yang, and Rozier, Kristin Yvonne. “Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems.” In IEEE/ACM 2014 International Conference on Computer-Aided Design (ICCAD), IEEE/ACM, November, 2014. DOI: 10.1109/ICCAD.2014.7001427 PDF IEEEXplore BibTeX Website Slides
  60. Johannes Geist, Kristin Yvonne Rozier, and Johann Schumann. “Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Systems.” In  14th International Conference on Runtime Verification (RV14), Springer-Verlag, Toronto, Canada, September 22-25, 2014. DOI:10.1007/978-3-319-11164-3_18 PDF (Proceedings version: PDF)  BibTeX  Experiments/Downloads
  61. Rozier, Kristin Yvonne, and Rozier, Eric. “Reproducibility, Correctness, and Buildability: the Three Principles for Ethical Public Dissemination of Computer Science and Engineering Research,” In IEEE International Symposium on Ethics in Engineering, Science, and Technology, Ethics’2014, May 23-24, 2014. PDF BibTeX Slides
  62. Badger, Julia, and Rozier, Kristin Yvonne, (Eds.): Proceedings of the Sixth NASA Formal Methods Symposium (NFM 2014), Houston, Texas, U.S.A., April 29-May 1, 2014. Lecture Notes in Computer Science (LNCS), volume 8430, Springer 2014. Springer Link BibTeX
  63. Thomas Reinbacher, Kristin Y. Rozier, and Johann Schumann. “Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems.” In 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 8413 of Lecture Notes in Computer Science (LNCS), pages 357–372, Springer-Verlag, Grenoble, France, 5-13 April 2014. PDF (Proceedings version: PDF) (Springer Link) BibTeX Tools and Simulation Traces
  64. Johann Schumann, Kristin Y. Rozier, Thomas Reinbacher, Ole J. Mengshoel, Timmy Mbaya, and Corey Ippolito. “Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for Unmanned Aerial Systems.” In 2013 Annual Conference of the Prognostics and Health Management Society (PHM2013), pages 381–401. October, 2013. PDF BibTeX
  65. Rozier, Kristin Y., and Vardi, Moshe Y. “Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking.” In 8th Haifa Verification Conference (HVC2012), volume 7857 of Lecture Notes in Computer Science (LNCS), pages 243–259, Springer-Verlag, 2012. PS PDF BibTeX Slides
  66. Zhao, Yang, and Rozier, Kristin Yvonne. “Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System.” In 12th International Workshop on Automated Verification of Critical Systems (AVoCS2012), volume 53, pages 43-57 of Electronic Communications of the EASST, 2012. DOI:10.14279/tuj.eceasst.53.787  PS PDF (Journal version: PDF)  BibTeX Software/Models
  67. Tabakov, Deian, Rozier, Kristin Y., and Vardi, Moshe Y. “Optimized Temporal Monitors for SystemC.” In Formal Methods in System Design Journal, volume 41, number 3, pages 236-268, Springer, January, 2012. PS (tarball) PDF (Journal version: PDF) BibTeX Software
  68. Rozier, Kristin Y., and Vardi, Moshe Y. “A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking.” In 17th International Symposium on Formal Methods (FM2011), volume 6664 of Lecture Notes in Computer Science (LNCS), pages 417–431. Springer-Verlag, 2011. PS PDF (Proceedings version: PDF) BibTeX  Slides Software
  69. Rozier, Kristin Y. “Linear Temporal Logic Symbolic Model Checking.” In Computer Science Review Journal, volume 5, number 2, pages 163-203, Elsevier, May, 2011. PDF BibTeX
  70. Rozier, Kristin Y., and Vardi, Moshe Y. “LTL Satisfiability Checking.” In International Journal on Software Tools for Technology Transfer (STTT), pages 123–137, Springer-Verlag, March, 2010. PS PDF (original LNCS publication: PDF)  BibTeX Software
  71. Rozier, Kristin Y., and Vardi, Moshe Y. “LTL Satisfiability Checking.” In14th Workshop on Model Checking Software (SPIN ’07), volume 4595 of Lecture Notes in Computer Science (LNCS), pages 149-167. Springer-Verlag, 2007. PS PDF (original LNCS publication: PDF)  BibTeX Software
  72. Burley, Casey L., Brooks, Thomas F., Rozier, Kristin Y., et al. “Rotor wake vortex definition evaluation of 3-C PIV results of the HART-II study,”International Journal of Aeroacoustics, volume 5, pages 1-38, January 2006. PDF BibTeX

Workshop Papers

  1. Varad V. Kulkarni, Allison L. Howard, Sydney R. V. Turner, Mukul S. Kulkarni, Nisha Raj, Eric A. Rasmussen, Mehmet B. Sefer, Karanvir Singh, and Kristin Y. Rozier. “OpenUAS: An OpenSource Unmanned Aircraft Systems (UAS) Testbed Solution under Cost Constraints.” AIAA Region V Student Conference, St. Louis, Missouri, USA, April 5–6, 2024. Won 2nd place in Student Research Competition, Team Category. DOI: 10.2514/6.2024-84417
  2. Justin Bradley, Cody Fleming, Kristin Y. Rozier, and Amy Pritchett. “Impact and Influence of Cyber-Physical Systems Research on Autonomous Aerospace Systems.” AIAA SciTech, National Harbor, Maryland, January 23–27, 2023. DOI: PDF BibTeX
  3. Sebastian Schirmer, Christoph Torens, Johann C. Dauer, Jan Baumeister, Bernd Finkbeiner, and Kristin Y. Rozier. “A Hierarchy of Monitoring Properties for Autonomous Systems.” AIAA SciTech, National Harbor, Maryland, January 23–27, 2023. DOI: 10.2514/6.2023-2588 PDF BibTeX
  4. Zachary A. Luppen, Dae Young Lee, and Kristin Yvonne Rozier. “A Case Study in Formal Specification and Runtime Verification of a CubeSat Communications System.” AIAA SciTech, Session on Formal Methods for Intelligent Aerospace Systems, Nashville, Tennessee, January 11–15, 2021. DOI: 10.2514/6.2021-0997 (Invited) PDF BibTeX
  5. Kristin Yvonne Rozier. “Temporal Logic Satisfiability From Specification Debugging to Benchmark Generation.” In Forth Women in Logic Workshop (WiL), June 30, 2020. PDF BibTeX Abstract Slides
  6. Wolfgang Ahrendt, Marieke Huisman, Giles Reger, and Kristin Yvonne Rozier. “A Broader View on Verification: From Static to Runtime and Back (Track Summary).” In 8th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA), volume 11245 of LNCS, pages 3-7, Springer, November, 2018. PDF BibTeX
  7. Rohit Dureja, Eric W.D. Rozier, and Kristin Y. Rozier. “A Case Study in Safety, Security, and Availability of Wireless-Enabled Aircraft Communication Networks.” In AIAA AVIATION, 5–9 June, 2017. PDF (Proceedings version: PDF) BibTeX

Technical Reports

  1. Kristin Yvonne Rozier and Giles Reger. “The International Runtime Verification Competition 2019.” Online: PDF
  2. Michael Lowry, Anupa Bajwa, Patrick Quach, Gabor Karsai, Kristin Y. Rozier, Sanjai Rayadurgam. “Autonomy Operating System for UAVs.” Online report, April 19, 2017. PDF NTRS BibTeX
  3. Kristin Yvonne Rozier, Johann Schumann, and Corey Ippolito. “Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS.” Technical Memorandum NASA/TM-2015-218817, May, 2015. PDF BibTeX

Magazine Articles

  1. Rozier, Kristin Yvonne. “Year In Review: Intelligent Systems,” Aerospace America, volume 52, number 11, page 45, December 2014. PDF BibTeX
  2. Rozier, Kristin Yvonne. “Year In Review: Intelligent Systems,” Aerospace America, volume 51, number 11, page 43, December 2013. PDF BibTeX
  3. Rozier, Kristin Yvonne. “Year In Review: Intelligent Systems,” Aerospace America, volume 50, number 11, page 42, December 2012. PDF BibTeX
  4. Rozier, Kristin Yvonne. “Year In Review: Intelligent Systems,” Aerospace America, volume 49, number 11, page 39, December 2011. PDF BibTeX
  5. Harvey, Seth, Ingham, Michel, Rozier, Kristin Yvonne. “Year In Review: Intelligent Systems,” Aerospace America, volume 48, number 11, page 41, December 2010. PDF BibTeX

Conference Proceedings

  1. Gidon Ernst, and Kristin Yvonne Rozier. (Eds.). Proceedings of the 31st International Symposium on Model Checking Software (SPIN). Lecture Notes in Computer Science (LNCS), volume TBD, Springer 2025. To appear: https://spin-web.github.io/SPIN2025/.
  2. André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi (Eds.). Proceedings of the 26th International Symposium on Formal Methods – FM 2024. Lecture Notes in Computer Science (LNCS), volumes 14933 and 14934, Springer 2024. To appear: https://www.fmeurope.org/symposia/.
  3. Rohit Dureja, Rosemary Monahan, and Kristin Yvonne Rozier, (Eds.): “High-Performance Computing and Formal Methods,” a volume of Frontiers in High Performance Computing Journal, 2024. https: //www.frontiersin.org/research-topics/50797/high-performance-computing-and-formal-methods
  4. Alexander Nadel, and Kristin Yvonne Rozier, (Eds.). Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023. Volume 4, pp. 1–317). TU Wien Academic Press, 2023. DOI: 10.34727/2023/isbn.978-3-85448-060-0.
  5. Kristin Yvonne Rozier and Swarat Chaudhuri, (Eds.): Proceedings of the Fifteenth NASA Formal Methods Symposium (NFM 2023), Houston, Texas, U.S.A., May 16–18, 2023. Lecture Notes in Computer Science (LNCS), volume 13903, Springer 2023, eBook ISBN 978-3-031-33170-1, Print ISBN 978-3-031-33169-5.
  6. Julia Badger and Kristin Yvonne Rozier. NASA Formal Methods: Proceedings of the 11th International Symposium, NFM 2019, volume 11460, Lecture Notes in Computer Science (LNCS), Springer International Publishing, May, 2019, DOI 10.1007/978-3-030-20652-9. Preface BibTeX
  7. Julia Badger and Kristin Yvonne Rozier. NASA Formal Methods: Proceedings of the 6th International Symposium, NFM 2014, volume 8430, Lecture Notes in Computer Science (LNCS), Springer International Publishing, April-May, 2014. BibTeX
  8. Rozier, Kristin Yvonne, ed.: Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM 2008), NASA/CP-2008-215309, May 2008. PDF BibTeX