5th Workshop on Cooperative Software Verification (COOP 2024)

At this point, the value and impact potential of formally verifying systems is undeniable. The list of formal methods success stories is long and full of unique contributions to not only verification but required elements for system utility such as certification, explainability, and automated reasoning. So why does the adoption of formal methods still pale in comparison to informal methods?

One major contributing factor is the primitive state of tool integration. Even the most advanced academic tools tend to be stand-alone software; roadblocks inhibiting integration include closed-source code, obscure or one-off input/output languages, lack of intuitive interfaces or user-facing documentation, and design flows prioritizing novelty over transparency. We take a look at challenges and opportunities in formal methods tool integration, centering our gaze on model checking. We highlight recent steps forward in unifying symbolic model checking, easing the specification bottleneck, and integrating runtime verification, and map out the next steps toward making it possible for formal verification to become as universal as informal verification.

Professor Kristin Yvonne Rozier heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University; previously she spent 14 years as a Research Scientist at NASA and three semesters as an Assistant Professor at the University of Cincinnati. She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Dr. Rozier's research focuses on automated techniques for the formal specification, validation, and verification of safety critical systems. Her primary research interests include: design-time checking of system logic and system requirements; runtime system health management; and safety and security analysis.

Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER Award; the NASA Early Career Faculty Award; American Helicopter Society's Howard Hughes Award; Women in Aerospace Inaugural Initiative-Inspiration-Impact Award; two NASA Group Achievement Awards; two NASA Superior Accomplishment Awards; Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award; Building a World of Difference faculty fellowship. She holds an endowed position as Dennis and Rebecca Muilenburg Professor, is an Associate Fellow of AIAA, and is a Senior Member of IEEE, ACM, and SWE. Dr. Rozier has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.