NASA Logo, National Aeronautics and Space Administration

Kristin Yvonne Rozier, Ph.D.

Selected Publications

  1. 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. To appear. PDF BibTeX Software/Models
  2. 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. To appear. PDF (Proceedings version: PDF) BibTeX Experiments/Downloads
  3. 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, Elsevier, 2014. To appear. PS PDF (Journal version: PDF) BibTeX Software/Models
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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, 2012. PS PDF (Journal version: PDF) BibTeX Software
  11. 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
  12. 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
  13. 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
  14. Rozier, Kristin Yvonne, ed.: Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM 2008), NASA/CP-2008-215309, May 2008. PDF BibTeX
  15. 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
  16. 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

Magazine Articles

Selected Technical Presentations

  • Keynote: Systers Lunch, an event affiliated with the Grace Hopper Celebration of Women in Computing (GHC 2014), Phoenix, Arizona, October 10, 2014.
  • Featured PI Presentation: "Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS." One of three NASA Aeronautics Research Institute (NARI) PI's featured as the 'best of' funded research for the 2012-2014 funding periods, presenting to over 250K members of the public at NASA Ames Open House, Moffett Field, California, October 18, 2014.
  • Featured Speaker: "No More Helicopter Parenting: Intelligent Autonomous Unmanned Aerial Systems." NASA Ames' premier seminar series, the Director’s Colloquium, special edition in honor of NASA Ames' 75th Anniversary celebration, by special invitation of the Office of the Chief Scientist. NASA Ames Research Center, Moffett Field, California, June 10, 2014. [Now available on the NASA Ames YouTube Channel under "Dr. Kristin Yvonne Rozier - No More Helicopter Parenting: Intelligent, Autonomous UAS" ]
  • Keynote: `"LTL Satisfiability Checking." Eighth International Workshop on Constraints in Formal Verification, a workshop affiliated with the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), San Jose, California, November 21, 2013.
  • "Formal Specification: Linear Temporal Logic and Applications in Runtime Monitoring." University of Miami, Department of Electrical and Computer Engineering EEN 417: Embedded Microprocessor System Design course invited lecture, September 25. 2013.
  • "Formal Specification: Linear Temporal Logic and Applications" and "Model Checking and Applications of Formal Methods at NASA." Invited lectures for graduate course EEN 513 - Software Design and Verification (a course based in part on Roz11), University of Miami, Department of Electrical and Computer Engineering, September 24-26, 2013.
  • "Formal Methods and Other Awesome Applications in Engineering." University of Miami, Department of Electrical and Computer Engineering EEN 112: Introduction to Engineering course invited lecture, March 6, 2013.
  • "Formal Specification and Verification: Linear Temporal Logic, State Machines, and Their Applications." University of Miami, Department of Electrical and Computer Engineering EEN 417: Embedded Microprocessor System Design course invited lectures, October 12. 2012.
  • "Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System at NASA." Univeristy of Miami, Invited College of Engineering Colloquium, Miami, Florida, October 10, 2012.
  • "Probabilistic Formal Verification of the Automated Airspace Concept High-Level Architecture." AFT/TI Seminar, NASA Ames Research Center, June 25, 2012. (A = Aeronautics Directorate; F = Aviation Systems Division; T = Flight Trajectory Dynamics and Controls Branch / TI = Intelligent Systems)
  • "Explicit and Symbolic Compilation of Linear Temporal Logic to Automata for Verification." PERFORM Performability Engineering Research Group Seminar Series, University of Illinois at Urbana-Champaign Coordinated Science Laboratory, Urbana, Illinois, February 17, 2012.
  • "A Multi-Encoding Approach for LTL Symbolic Satisfiability Checking," Invited symposium at Galois, Inc, Portland, OR, August 10, 2011, http://corp.galois.com/blog/.
  • "Formal Verification of the Automated Airspace Concept High-Level Architecture," AFT/TI Seminar, NASA Ames Research Center, May 9, 2011. (A = Aeronautics Directorate; F = Aviation Systems Division; T = Flight Trajectory Dynamics and Controls Branch / TI = Intelligent Systems)
  • "Formal Methods for NGATS System Verification Explained," NGATS Airspace AFT Seminar, NASA Ames Research Center, November 2, 2009. (A = Aeronautics Directorate; F = Aviation Systems Division; T = Flight Trajectory Dynamics and Controls Branch)
  • "Formal Methods Explained," University of Nevada at Reno Computer Science & Engineering Colloquium Series, Reno, Nevada, October 29, 2009.
  • "Solving the Two Body Problem," Panel organizer and panelist with Katy Dickinson (Sun Microsystems), Amarda Shehu (George Mason University), Evgenia Smirni (College of William and Mary). Grace Hopper Celebration (GHC) of Women in Computing Conference, Tucson, Arizona, September 30-October 3, 2009. (Presentation 1:45PM - 2:45PM on Oct. 2.)
  • "Women and the Flat Connected World," Panel with Meenakshi Kaul-Basu (Sun Microsystems), Bev Crair (Quantum Corporation), Claudia Galván (Microsoft Corporation), Lydia Ash (Google), Radha Ratnaparkhi (IBM), Sumitha Prashanth (Sun Microsystems). Grace Hopper Celebration (GHC) of Women in Computing Conference, Tucson, Arizona, September 29-October 3, 2009. (Presentation 11:15AM - 12:15PM on Oct. 1.)
  • "MAGIC: Setting Up An Effective Organization To Support Girls," Birds of a Feather (BOF) with Ira Pramanick, Fauzia Saeed, Katy Dickinson, Meenakshi Kaul-Basu, and Robin Wilensky. Grace Hopper Celebration (GHC) of Women in Computing Conference, Keystone Resort, Colorado, October 1-4, 2008. (Presentation 5:10PM - 6:10PM on Oct. 3.)
  • "Choosing Your Building Bricks: How to Find Your Research Direction," Presentation with Kristen R. Walcott and Katie Panciera. Grace Hopper Celebration (GHC) of Women in Computing Conference, Keystone Resort, Colorado, October 1-4, 2008. (Presentation 2:50PM - 3:50PM on Oct. 3.)
  • "On Formal Methods." Longwood University Mathematics & Computer Science Colloquium Series, Farmville, Virginia, September 4, 2008.
  • "Life-Critical System Verification." Visions for Theoretical Computer Science Workshop (TCS Visions), Seattle, Washington, May 17, 2008. Contributed to several nuggets; see Life-Critical System Verification in particular.
  • "Career Life Balance." Committee on the Status of Women in Computing Research (CRA-W) 2008 Grad Cohort Program for Women, Seattle, WA, March 13-14, 2008. Slides
  • "Symbolic LTL Compilation for Model Checking." Grace Hopper Celebration (GHC) of Women in Computing Conference, Orlando, Florida, October 17-20, 2007.
  • NGATS Airspace API/Researcher Meeting Featured Presentation, NASA Langley Research Center, June 27, 2007.
  • Safety Critical Avionics Systems Branch Talk, NASA Langley Research Center, September 20, 2006.
  • "Algorithms for Automata-Theoretic Linear Temporal Logic Model Checking." Games and Verification (GAMES 2006), July 3-7, 2006.
  • "Algorithms for Automata-Theoretic LTL Model Checking." Cambridge University Automated Reasoning Group(ARG) Lunch Lecture Series, June 28, 2006.
  • Safety Critical Avionics Systems Branch Talk, NASA Langley Research Center, June 6, 2005.
  • "Hypatheon Group Report," Assessment Technology Branch Talk, NASA Langley Research Center, July, 2004.

Conference Organizations

Women in Computer Science Conferences

Acknowledgments In Books


Kristin is proud to have contributed useful comments to the following publications:
  1. Valasek, John (ed), Advanced Intelligent and Autonomous Aerospace Systems, American Institute of Aeronautics and Astronautics, October, 2012.
  2. Lawrence M. Leemis and Stephen K. Park, Discrete-Event Simulation: A First Course, Prentice-Hall, Inc.,Upper Saddle River, NJ, USA, 2005. (ISBN 0131429175). BibTeX

Professional Service


Dr. Rozier regularly serves on peer-review and award panels and contributes to the numerous outreach and volunteer programs sponsored by or associated with NASA and the local scientific community.
First Gov logo
NASA Logo - nasa.gov