Department of Aerospace Engineering & Engineering MechanicsDepartment of Aerospace Engineering & Engineering MechanicsDepartment of Aerospace Engineering & Engineering MechanicsCollege of Engineering & Applied ScienceUniversity of Cincinnati

Department of Aerospace Engineering & Engineering Mechanics

Kristin Yvonne Rozier

Kristin Yvonne Rozier

Dr. Kristin Yvonne Rozier, Assistant Professor
PhD in Computer Science from Rice University, 2012

Contact Information:
Room Location: 727 Rhodes Hall
Phone Number: 513-556-3544
E-Mail Address: rozierky@ucmail.uc.edu

Web Site:  http://laboratory.temporallogic.org

NASA Web Site:  http://ti.arc.nasa.gov/profile/kyrozier/



NSF CAREER Award winner and recipient of the Inaugural Initiative-Inspiration-Impact Award from Women in Aerospace, Kristin Yvonne Rozier joined the faculty of the Aerospace Engineering and Computer Science Departments in Spring, 2015. Previous to that, she 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). 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.

Research Interests

  • Formal methods, verification and validation of safety-critical systems.
  • Design-time checking of system logic and system requirements with applications in aerospace systems, automated control, biomedical privacy, secure protocols.
  • System and safety health management for intelligent, autonomous Unmanned Aerial Systems.
  • 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.

Awards and Honors

  • NSF CAREER Award "CAREER: Theoretical Foundations of the UAS in the NAS Problem (Unmanned Aerial Systems in the National Air Space),'' 2016
  • Faculty Fellow, Eric & Wendy Schmidt Data Science for Social Good Summer Fellowship, Computation Institute, University of Chicago, Chicago, Illinois. (summer, 2015)
  • Darwin T. Turner Scholars Program Breakfast of Champions Faculty Medal from University of Cincinnati,  for work in mentoring and nurturing female and under-represented minority students; nominated by a student "as someone who deserves to be acknowledged for their hard work and dedication" 2015.
  • NASA Group Achievement Award (Prognostics Team) 2014 "For groundbreaking foundational discoveries in the field of Prognostics and Health Management."
  • Above and Beyond Award (co-recipient as part of NASA Ames) from the Society for Women Engineers, for outstanding dedication and impact in engineering outreach during the year 2013-2014
  • Initiative-Inspiration-Impact Award from Women in Aerospace "For exemplary achievement of formal specification, verification, and validation of a NextGen air traffic control system candidate and for dedication as a mentor and role model." (This prestigious award is presented for an individual in her early career, who consistently surpasses expectations from a technical, interpersonal, and management perspective, commitment to professional growth, and service as a role model or mentor that shows dedication to the advancement of women in aerospace.) 2013
  • Distinguished Service Award from the American Institute of Aeronautics and Astronautics Intelligent Systems Technical Committee "For Significant Contributions to the Activities of the ISTC and AIAA." 2008-2013
  • NASA Superior Accomplishment Award for "Outstanding leadership in planning and executing the Sixth NASA Langley Formal Methods Workshop.'' 2008
  • NASA Superior Accomplishment Award from the Contractors Steering Council for contributions to NASA's Aerospace Careers Program for Middle Schools, Spring, 2003
  • Howard Hughes Award from the American Helicopter Society "For contributions to the automation, capability for version control, and flight data organization for validation of the NASA TiltRotor Aeroacoustics Code (TRAC) as a part of the development team." 2002
  • NASA Group Achievement Award (TRAC System and Analysis Team) 2002
  • Lockheed Martin Space Operations Lightning Award 2002
  • Phi Beta Kappa inducted 05/2000
  • James Monroe Scholar, College of William and Mary. 1996-2000

Selected Publications

  1. 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
  2. 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, IEEE, Austin, Texas, USA, November 5, 2015. (Invited) PDF BibTeX
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. Rozier, Kristin Yvonne, ed.: Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM 2008), NASA/CP-2008-215309, May 2008. PDF BibTeX
  21. 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
  22. 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

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

Selected Technical Presentations

  • TBD, invitation-only workshop on the ``Theoretical Foundations of SAT Solving,'' Fields Institute, Toronto, Canada, August 15-19, 2016. 
  • Seminar, Tutorial, and Short-term visit: ``Linear Temporal Logic Satisfiability Checking,'' Theory Reading Group,  KTH Royal Institute of Technology, Stockholm, Sweden, December 14--18, 2015.
  • Keynote: ``Layers of Formal Verification for Full-Scale NextGen Automated Air Traffic Control,'' Layered Assurance Workshop (LAW). Los Angeles, California, December 7--8, 2015.
  • EECS Department Research Seminar, University of Cincinnati, November 30, 2015.
  • "Formal Methods!'' University of Cincinnati, EECE 6032-Software Testing and Quality Assurance course invited lecture, November 20, 2015.
  • ``From Planes to UAS: Safe, Automated Air Traffic Control.'' Grace Hopper Celebration (GHC) October 14-16, 2015.
  • ``Symbolic Model Checking for Full-Scale Design Space Exploration of NextGen Automated Air Traffic Control.'' CAVR Seminar, Rice University, October 14, 2015.
  • ``Intelligent Autonomous Unmanned Aerial Systems (UAS) and R2U2: a System Health Management Framework.'' University of Cincinnati Seminar, October 8, 2015. 
  • Keynote: Safe and Secure Systems and Software Symposium (S5), sponsored by the Air Force Research Laboratory (AFRL), Dayton, Ohio, June 10, 2015.
  • ``Linear Temporal Logic Satisfiability Checking.'' Dagstuhl Seminar 15171, ``Theory and Practice of SAT Solving'' April 19-24, 2015.
  •  ``Formal Methods: Designing Safety-Critical Aerospace Systems at the University of Cincinnati.'' Presentation at UC AEEM Advisory Board Meeting, April 17, 2015.
  • ``Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS.'' Poster and Presentation at College Advisory Council Meeting, April 10, 2015.
  • ``Formal Methods!'' University of Cincinnati, EECE 6032-Software Testing and Quality Assurance course invited lecture, March 31, 2015.
  • ``Crazy Idea: Net-Enabled Aircraft!'' Invited Symposium at SRI's Crazy Idea Friday, March 20, 2015.
  •  Research presentation at AEEM graduate student recruitment weekend, University of Cincinnati, March 7, 2015.
  • ``Formal Methods! Designing Safety-Critical Systems at University of Cincinnati.'' Invited Symposium at University of Victoria's ``Women in Engineering and Computer Science'' Symposium series, February 27, 2015.
  • ``Formal Methods Challenge: Efficient Reconfigurable Cockpit Design and Fleet Operations using Software Intensive, Networked, and Wireless-Enabled Architecture (ECON).'' Dagstuhl Seminar 15071, ``Formal Foundations for Networking,'' February 8-13, 2015.
  • ``Formal Methods! Join the Laboratory for Temporal Logic at UC.'' Featured faculty speaker at joint AIAA/ACM-W student chapters meeting, February 3, 2015.
  • ``Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS'' with Johann Schumann and Corey Ippolito. 2015 NARI LEARN/Seedling Technical Seminar, January 13, 2015.
  • 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
  • ``Women in STEM Career Talk'' Santa Clara University Women in STEM club, November 20, 2014.
  • "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" ]
  • ``From Design Time To Run Time: Formal Methods for Ensuring the Safety of Safety-Critical Aerospace Systems.'' University of Cincinnati Aerospace Engineering Seminar, Cincinnati, Ohio, May 19, 2014.
  • ``From Design Time To Run Time: Formal Methods for Ensuring the Safety of Safety-Critical Aeronautics Systems.'' Tulane Computer Science Seminar, New Orleans, Louisiana, April 23, 2014.
  • ``From Design Time To Run Time: Formal Methods for Ensuring the Safety of Safety-Critical Aeronautics Systems.'' Arizona State University Computer Science Seminar, Tucson, Arizona, April 17, 2014.
  • ``Advances in Linear Temporal Logic Translation: Ensuring the Safety of Safety-Critical Aeronautics Systems.'' Montana State University Computer Science Department Seminar, Bozeman, Montana, March 28, 2014.
  • 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 STEM Conferences

Acknowledgments In Books


Dr. Rozier 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.