Publications

Publications (Peer-Reviewed)

  1. 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 PDF BibTeX Website
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  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, 2020. PDF BibTeX Video
  8. 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. PDF BibTeX Website EasyChair-SmartSlides Short Video Long Video
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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. PDF BibTeX Website Video
  22. 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 Slides
  23. 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
  24. 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 Journal Version BibTeX
  25. 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 BibTeX
  26. 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. PDF BibTeX Website Demo
  27. 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. (Received the “Artifact Evaluated Stamp” — highest mark from Artifact Evaluation Review Committee http://barghouthi.github.io/cav16-aec/) PDF BibTeX Website&Models
  28. 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) PDF BibTeX
  29. 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
  30. 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
  31. 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. PDF BibTeX Slides
  32. 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. PDF BibTeX
  33. 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. PDF BibTeX
  34. 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. PDF BibTeX
  35. 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 PS PDF (Journal version: PDF) BibTeX Software/Models
  36. 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. PDF BibTeX Software/Models Slides
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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 Software
  46. 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
  47. 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
  48. Rozier, Kristin Y., and Vardi, Moshe Y. “LTL Satisfiability Checking.” In14th Workshop on Model Checking Software (SPIN ’07), volume 4595 ofLecture Notes in Computer Science (LNCS), pages 149-167. Springer-Verlag, 2007. PS PDF (original LNCS publication: PDF) BibTeX Software
  49. 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

  • 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: https://doi.org/10.2514/6.2021-0997 (Invited) PDF BibTeX
  • 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
  • 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, Veri cation, and Validation (ISoLA), volume 11245 of LNCS, pages 3-7, Springer, November, 2018. PDF BibTeX
  • 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

  • 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
  • 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

Conference Proceedings