Kristin Yvonne Rozier - Publications

Kristin Yvonne Rozier, Ph.D.

Selected Publications

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 TBD of Lecture Notes in Computer Science (LNCS). Springer-Verlag, 2012. PS PDF BibTeX
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
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
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
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
Rozier, Kristin Y., and Vardi, Moshe Y. "LTL Satisfiability Checking." In International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag, March, 2010. PS PDF (original LNCS publication: PDF) BibTeX Software
Rozier, Kristin Yvonne, ed.: Proceedings of the Sixth NASA Langley Formal Methods Workshop (LFM 2008), NASA/CP-2008-215309, May 2008. PDF BibTeX
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
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

Rozier, Kristin Yvonne. "Year In Review: Intelligent Systems," Aerospace America, volume 50, number 11, page 42, December 2012. PDF BibTeX
Rozier, Kristin Yvonne. "Year In Review: Intelligent Systems," Aerospace America, volume 49, number 11, page 39, December 2011. PDF BibTeX
Harvey, Seth, Ingham, Michel, Rozier, Kristin Yvonne. "Year In Review: Intelligent Systems," Aerospace America, volume 48, number 11, page 41, December 2010. PDF BibTeX

Technical Presentations

"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.
"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

April 29 - May 1, 2014: PC Chair, Steering Committee, The Sixth NASA Formal Methods Symposium (NFM 2014), Houston, Texas, USA.
September 11-13, 2013: Programme Committee, 13th International Workshop on Automated Verification of Critical Systems (AVoCS 2013), Surrey, UK.
August 14-16, 2013: Programme Committee, The IEEE International Workshop on Formal Methods Integration (FMi 2013), San Francisco, California, USA.
June 12-14, 2013: Programme Committee, The 10th International Conference on Integrating Formal Methods (iFM 2013), Turku, Finland.
May 14-16, 2013: Steering Committee, Program Committee, The Fifth NASA Formal Methods Symposium (NFM 2013), Moffett Field, California, USA.
January 8, 2013: Steering Committee, Program Committee, Software Challenges in Aerospace, Grapevine, Texas, USA.
October 12-13, 2012: Program Committee, 35th Annual IEEE Software Engineering Workshop (SEW-35), Heraclion, Crete, Greece.
April 3-5, 2012: Steering Committee, Program Committee, Session Chair, The Forth NASA Formal Methods Symposium (NFM 2012), Norfolk, Virginia, USA.
June 20-21, 2011: Program Committee, 34th Annual IEEE Software Engineering Workshop (SEW-34), Limerick, Ireland.
April 18-20, 2011: Steering Committee, Program Committee, Session Chair, The Third NASA Formal Methods Symposium (NFM 2011), Pasadena, California, USA.
March 29-31, 2011: Program Co-chair (with Ufuk Topcu and Nok Wongpiromsarn) Verification and Validation of Aerospace Systems Focused Session, AIAA Infotech@Aerospace, St. Louis, Missouri, USA.
April 20-22, 2010: Program Co-chair (with Stephen A. Jacklin) Verification and Validation of Aerospace Systems Focused Session, AIAA Infotech@Aerospace, Atlanta, Georgia, USA.
2010: PC/Review committee for NFM 2010 special issue of the NASA Journal, Innovations in Systems and Software Engineering (ISSE)
April 13 - 15, 2010: Organizing Committee, Program Committee, Session Chair, The Second NASA Formal Methods Symposium (NFM 2010), Washington, DC, USA.
2009: PC/Review committee for NFM 2009 special issue of the NASA Journal, Innovations in Systems and Software Engineering (ISSE)
April 6 - 8, 2009: Organizing Committee, Program Committee, Session Chair, The First NASA Formal Methods Symposium (NFM 2009), Moffett Field, CA, USA.
May 17, 2008: Co-chair (with Amit Sahai) of the breakout group on Security, Privacy, and Reliability at the Visions for Theoretical Computer Science (TCS) Workshop, Seattle, Washington, USA.
April 30-May 2, 2008: General Chair, The Sixth NASA Langley Formal Methods Workshop (LFM 2008), Newport News, VA, USA.

Women in Computer Science Conferences

9th Grace Hopper Celebration (GHC) of Women in Computing Conference, Tucson, Arizona, September 30-October 3, 2009.
8th Grace Hopper Celebration (GHC) of Women in Computing Conference, Keystone Resort, Colorado, October 1-4, 2008.
Committee on the Status of Women in Computing Research (CRA-W) 2008 Grad Cohort Program for Women, Seattle, WA, March 13-14, 2008.
7th Grace Hopper Celebration (GHC) of Women in Computing Conference, Orlando, Florida, October 17-20, 2007.
Committee on the Status of Women in Computing Research (CRA-W) 2007 Grad Cohort Program for Women, San Francisco, California, March 2-3, 2007.
6th Grace Hopper Celebration (GHC) of Women in Computing Conference, San Diego, California, October 4-7, 2006.
WWW2006 BCSWomen and Women@CL Career Development Workshop 2006, Edinburgh, Scotland, May 22nd 2006.
Committee on the Status of Women in Computing Research (CRA-W) 2005 Grad Cohort Program for Women, San Francisco, California, February 25-26, 2005.

Acknowledgments In Books

Kristin is proud to have contributed useful comments to the following publications:

Valasek, John (ed), Advanced Intelligent and Autonomous Aerospace Systems, American Institute of Aeronautics and Astronautics, October, 2012.
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

Kristin 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.

Mentor, The Huffington Post's Girls in STEM mentorship program (2013)
Reviewer, Innovations in Systems and Software Engineering (ISSE): A NASA Journal, Special Issue on Software Health Management (SI: SwHM) (4/2013)
Reviewer, 9th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE) (2013)
Reviewer, 25th International Conference on Computer Aided Verification (CAV) (2013)
Reviewer, 24th International Conference on Automated Deduction (CADE-24) (2013)
NASA Technical Recruiter for Undergraduate and Graduate Students: 2013 Winter Engineering Career Fair at Santa Clara University (1/16/2013), San Jose State University Expo '13 (2/26/2013)
Mentor for WitsOn (Women in Technology Sharing Online), a Harvey Mudd College and Piazza pilot mentoring project to connect undergraduates pursuing STEM degrees with female mentors from industry and academia who can speak from personal experience about issues of particular concern to young women (10-11/2012)
Reviewer, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2013)
Reviewer, 14th International Conference on. Verification, Model Checking, and Abstract Interpretation (VMCAI) (2013)
Reviewer, Science of Computer Programming Journal, Elsevier (9/2012)
Proposal Reviewer, NASA Solicitation and Proposal Integrated Review and Evaluation System (NSPIRES) (6/2012)
Reviewer, The 19th International SPIN Workshop on Model Checking of Software (SPIN) (2012)
Reviewer, The 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18) (2012)
Reviewer, The 3rd International Conference on Verified Software: Theories, Tools and Experiments (VSTTE) (2012)
NASA speaker at Mountain View High School's College Awareness Day Career Fair (10/12/11)
Reviewer, 13th International Conference on. Verification, Model Checking, and Abstract Interpretation (VMCAI) (2012)
Reviewer, Automated Technology for Verification and Analysis (ATVA) (2011)
Head Judge, Inaugural AIAA Intelligent Systems Award, Santa Clara Valley Science and Engineering Fair Synopsys Championship (3/9/11, 4/3/11, 3/7/12, 3/13/13)
Santa Clara Valley Science and Engineering Fair 2011 Mentor
AIAA Intelligent Systems Award Selection Panel: "The Selection Panel will include 4 additional members to be appointed by the ISTC Chair. These appointees shall be nationally recognized experts in areas relevant to ISTC scope, and should be members of AIAA in good standing, but need not be current members of ISTC." (2010)
Reviewer, Elsevier Computer Science Review Journal (11/2011)
Proposal Reviewer, NASA Minority-Serving Institution Faculty Engagement Competition (11/2011)
Proposal Reviewer, NASA Small Business Innovation Research (SBIR), http://sbir.gsfc.nasa.gov/SBIR/SBIR.html, Phase I and Phase II proposals (10/2011, 10/2012, 01/2013, 02/2013)
Reviewer, 23rd International Conference on Computer Aided Verification (CAV) (2011)
Reviewer, ACM SIGSOFT 19th International Symposium on the Foundations of Software Engineering (FSE) (2011)
Reviewer, NFM 2010 special issue of the NASA Journal, Innovations in Systems and Software Engineering (ISSE) (2010)
Reviewer, SPIN 2010: 17th International SPIN Workshop on Model Checking of Software (2010)
Reviewer, AIAA Journal of Aerospace Computing, Information, and Communication (JACIC) (2010)
NASA speaker at Peninsula Girl Scout Day Camp, Huddart Park, presented to 150 teens aged 12-18 years (7/21/2010)
AIAA Intelligent Systems Technical Committee (ISTC) Publications Subcommittee (member: 6/2008 - present; chair: 7/2010-present)
NASA speaker for EPATT (East Palo Alto Tennis and Tutoring) Lunchtime Speaker Series event, 3rd-6th grade groups (6/29/10)
National Center for Women & Information Technology (NCWIT) Award for Aspirations in Computing Judge (April-May/2010, Oct-Nov/2010, Nov/2011)
NASA Event Staff, 35th Annual Sunnyvale Art and Wine Festival (6/6/2009), 36th Annual (6/6/2010)
Reviewer, "Annals of Mathematics in Artificial Intelligence" (AMAI) for the topic area "Formal Methods in Aerospace" (2010)
AIAA Intelligent Systems Book: chair of peer-review committee, invited peer reviewers, coordinated all book chapter reviews, other organizational tasks
Reviewer, Intelligent Systems Track, 48th AIAA Aerospace Sciences Meeting (ASM) (2010)
Reviewer, Formal Methods in Computer Aided Design (FMCAD) (2009)
Reviewer, NFM 2009 special issue of the NASA Journal, Innovations in Systems and Software Engineering (ISSE) (2009)
Reviewer, AIAA Journal of Aerospace Computing, Information, and Communication (JACIC) (2009)
Intel International Science and Engineering Fair 2009 Judge, Reno, Nevada (5/12-13/2009)
Reviewer, ACM Transactions on Software Engineering and Methodology (TOSEM) Journal (2009, 2013)
16th Annual NASA Ames Student Space Settlement Design Contest Judge (4/23/09), 17th Annual (4/20/10)
AIAA/NASA Ames Research Center Galileo High School Scholarship Evaluator (April-May/2009, March-May/2010)
Santa Clara Valley Science and Engineering Fair Synopsys Championship Judge (3/18/09, 3/17/10)
Girls Achieving in Non-traditional Subjects (GAINS) "Lunch with a NASA Scientist" (2/17/09)
NASA Combined Federal Campaign (CFC) key worker 2008
NASA Event Staff, Airship Ventures Dedication/Moffett 75th Diamond Jubilee Ceremony, Moffett Field, CA (11/21/2008)
NASA representative, Smithsonian Folklife Festival, Washington, DC (7/3/2008)
AIAA Intelligent Systems Technical Committee (ISTC) Professional Development & Outreach Subcommittee (member: 6/2008 - present; chair: 7/2009-present)
Virginia Junior Academy of Science (VJAS) Computer Science Judge (5/21/2008)
Gildersleeve Science Fair Judge (12/13/2007)
Reviewer, ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation: Special Workshop Theme: Formal Methods in Avionics, Space and Transport (10/2007)
MAGIC (More Active Girls In Computing) core team member/mentor (10/2007-8/2010)
NASA Exhibition Trailer staff at Air Power Over Hampton Roads, Langley AFB (4/28/2007)
NASA representative at the Virginia Air and Space Center SpaceQuest Opening (4/21/2007)
eCYBERMISSION Judge (3/2007)
CHROME Club Speaker at Jones Middle School (2/12/2007), Eaton Middle School (6/07/2007)
York County Regional Science Fair Judge at Bruton High School (1/31/2007), Grafton High (1/31/2008)
River Oaks Baptist School of Houston Science Fair Judge (11/17/2005)
Workshop Leader and Speaker: "Just Plane Wings," Girl Scout Day (a day for Brownie Girl Scouts to learn about science), Rice University (11/12/2005)
Tidewater Regional Science Fair Judge (3/20/2004, 3/08/2008)
Menchville High School Science Fair Judge (12/09/2003, 12/11/2006, 12/06/2007)
National Space Day presenter, McIntosh Elementary (5/1/2003)
Newport News All City Science Fair Computer Science Judge (1/25/2003, 1/31/2004, 1/20/2007, 1/12/2008)
Dozier Middle School Science Fair Engineering Judge (12/5/2002)
New Horizons Governor's School for Science and Technology presentation observer (5/2/2002) and judge (5/2/2003, 4/29/2004)
Virginia State Science and Engineering Fair Computer Science Judge, Randolph-Macon College (4/13/2002, 4/5/2003), George Mason University (CS Chair: 4/12/2008)
NASA "Careers in Aerospace" Speaker: Dozier Middle School (4/11/2002), Hines Middle School (3/13/03), Jones Magnet School (twice: 4/8/2004), Reservoir Middle School (3/13/2007)
Gloucester High School Senior Project advisor (2001-2)