Kristin Yvonne Rozier

Kristin Yvonne Rozier

Affiliation:
Associate Professor of Aerospace Engineering & Computer Science
Iowa State University, USA

Title: The Temporal Logic of Flight
Abstract:
Verification of aerospace systems has consistently been one of the core, driving domains for formal methods since the inception of this field. So, how have we done in practice? This keynote will present a flight-system perspective on formal representation of time. We will discuss the collection of real-life, full-scale flight system formal verification success stories across the field, examine the concept of time in aerospace operational concepts, and take stock of the current gaps between formal methods research and flight system practice. Looking to the future, we will call out research questions we must answer as formal methods strive to boldly go where no human has gone before.

Kristin Yvonne Rozier is a researcher in formal methods, automated reasoning, and verification of safety-critical systems. She leads the Laboratory for Temporal Logic at Iowa State University and previously worked as a research scientist at NASA.

Personal webpage:
https://www.aere.iastate.edu/kyrozier/

Alessandro Cimatti (talk shared with DX 2026)

Alessandro Cimatti

Affiliation:
Director, Digital Industry Center
Fondazione Bruno Kessler (FBK), Italy

Title: From Runtime Verification to Model Based Diagnosis
Abstract:
TBA

Alessandro Cimatti is Director of the Digital Industry Center at Fondazione Bruno Kessler. He is a leading researcher in formal methods and artificial intelligence, known for his contributions to bounded model checking and automated reasoning.

Personal webpage:
https://dicenter.fbk.eu/contacts/alessandro-cimatti/