Publications

Publications (Peer-Reviewed)

  1. 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. PDF BibTeX Website
  2. Jianwen Li, Kristin Yvonne Rozier, and Moshe Vardi. “Satis ability Checking for Mission-Time LTL.”In Proceedings of the 31st International Conference on Computer Aided Veri fication (CAV), Springer-Verlag, New York, New York, USA, July 15-18, 2019. PDF BibTeX
  3. 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 TBD of Lecture Notes in Computer Science (LNCS), pages TBD, Springer-Verlag, New York, New York, USA, July 13–14, 2019. PDF BibTeX Website
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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 Video
  10. 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. PDF BibTeX Slides
  11. 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. PDF BibTeX 
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. Rozier, Kristin Yvonne, ed.: Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM 2008), NASA/CP-2008-215309, May 2008. PDF BibTeX
  37. 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
  38. 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

  • Wolfgang Ahrendt, Marieke Huisman, Giles Reger, and Kristin Yvonne Rozier. “A Broader View on Verifi cation: 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

  • 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