Dr. Kristin Y. Rozier gave two invited lectures for the graduate course on Software Design and Verification at the University of Miami. The course was newly designed this year by Professor Saman Zonouz based on a set of prominent research papers including one by Dr. Rozier:
Rozier, Kristin Y. “Linear Temporal Logic Symbolic Model Checking.” In Computer Science Review Journal, volume 5, number 2, pages 163-203, Elsevier, May, 2011
Dr. Rozier was asked to give lectures based on her paper to kick off two sections of the course; one lecture was on “Formal Specification: Linear Temporal Logic and Applications;” and the other lecture was on “Model Checking and Applications of Formal Methods at NASA.”
Dr. Rozier also delivered a third invited lecture aimed at an undergraduate audience for the Embedded Microprocessor System Design course in the Department of Electrical and Computer Engineering. She instructed the class on the subjects of temporal logic and formal specification, and included applications such as runtime monitoring. She tied the material in the students' text to her research and real-life successes in formal verification at NASA.
BACKGROUND: Dr. Kristin Yvonne Rozier is a research computer scientist contributing research to the Next Generation Air Transportation System (NextGen) Air Traffic Management project of the Airspace Systems Program, focusing on automated techniques for formal specification and verification of safety critical systems.
NASA PROGRAM FUNDING: Separation Assurance Research Focus Area, Airspace Systems Program
Contact: Kristin Y. Rozier