Publications

Publications (Peer-Reviewed)

  1. Rohit Dureja and Kristin Yvonne Rozier. “FuseIC3: An Algorithm for Checking Large Design Spaces.” In Formal Methods in Computer-Aided Design (FMCAD 2017), IEEE/ACM, Vienna, Austria, October 2-6, 2017. PDF BibTeX Slides
  2. 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 BibTeX
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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. PS PDF (Journal version: PDF) BibTeX Software/Models
  14. 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
  15. 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. PDF (Proceedings version: PDF) BibTeX Experiments/Downloads
  16. 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
  17. 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. BibTeX
  18. 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) BibTeX Tools and Simulation Traces
  19. 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
  20. 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
  21. 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 of Electronic Communications of the EASST, 2012. PS PDF (Journal version: PDF) BibTeX Software/Models
  22. 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 PDF (Journal version: PDF) BibTeX Software
  23. 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
  24. 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
  25. 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
  26. Rozier, Kristin Yvonne, ed.: Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM 2008), NASA/CP-2008-215309, May 2008. PDF BibTeX
  27. 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
  28. 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

  • 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

  • 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