Faculty and Staff Directory

Kristin Yvonne Rozier

  • Assistant Professor
  • Courtesy Appointment to the Department of Computer Science
  • Courtesy Appointment to the Department of Electrical and Computer Engineering

Main Office

2335 Howe Hall
Ames, IA 50011
Phone: 515-294-6956




Education

2012 - Rice University Ph.D. in Computer Science

2001 - College of William and Mary M.S. in Computer Science

2000 - College of William and Mary B.S. in Computer Science, Magna Cum Laude

Interest Areas

Formal methods, verification and validation of safety-critical systems; Design-time checking of system logic and system requirements with applications in aerospace systems, biomedical privacy, secure protocols; Model checking, property-based design, model-based design; Linear Temporal Logic satisflability checking, specification debugging techniques and theory; Automated reasoning, runtime monitoring, fault tolerance and safety analysis.

Brief Biography

Recipient of the Inaugural Initiative-Inspiration-Impact Award from Women in Aerospace, Kristin Yvonne Rozier joined the faculty of the Department of Aerospace Engineering in the Summer of 2016. Prior to that, She was an assistant professor of aerospace engineering and computer science at the University of Cincinnati. Rozier spent 14 years as a Research Scientist at NASA, holding civil service positions at NASA Ames Research Center (2008-2014) and NASA Langley Research Center (2001-2008).

Rozier earned her PhD in Computer Science from Rice University and MS and BS degrees from the College of William and Mary. During her tenure at NASA, she contributed research to the Aeroacoustics, and Safety-Critial Avionics groups at NASA Langley and to the Robust Software Engineering, and Discovery and Systems Health groups in the Intelligent Systems Division at NASA Ames. She has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.

Most recently, Rozier was a primary contributing researcher to the Next Generation Air Transportation System (NextGen) Air Traffic Management project of the Airspace Systems Program at NASA. She also served as Principal Investigator of an ARMD Seedling project advancing System and Safety Health Management for Unmanned Aerial Systems (UAS). In 2016, Rozier was the recipient of an NSF Career Award. Rozier will help to build a safer national air space with increased capacity for UAS and create broadly impactful capabilities for System Health Management (SHM) on-board UAS, thus ensuring the safety of people and property on the ground.

Select the following link for Roziers NASA Ames presentation: "Dr. Kristin Yvonne Rozier - No More Helicopter Parenting: Intelligent, Autonomous UAS."

Rozier is an Associate Fellow of AIAA and a Senior Member of IEEE and SWE.

Selected Publications

  1. 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. PSPDF (Journal version: PDF) BibTeX Software/Models
  2. 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 BibTeXSoftware/Models Slides
  3. 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
  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 ofElectronic Communications of the EASST, 2012. PS PDF (Journal version: PDF) BibTeXSoftware/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, January, 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

  • Invited: "Integration of Formal Methods into Design and Implementation of Aerospace Systems." CPS Verification & Validation: Industrial Challenges & Foundations, Carnegie Mellon University, December 11-12, 2014. Abstract Slides
  • "Probabilistic Model Checking for Comparative Analysis of Automated Air Traffic Control Systems," AFT Seminar, NASA Ames Research Center, October 27, 2014. (A = Aeronautics Directorate; F = Aviation Systems Division; T = Flight Trajectory Dynamics and Controls Branch)
  • 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 150K members of the public at NASA Ames Open House, Moffett Field, California, October 18, 2014.
  • Panelist: ``Ask a NASA Expert.'' Served on two panels of six experts (11am & 3pm), 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.