Program

Sunday, April 07, Room Ansembourg

Session 1: Opening and Keynote
  • Opening
  • Keynote: Challenges in Tool Integration: Making Formal Methods Universal (PDF)
    Speaker:
    Kristin-Yvonne Rozier (Iowa State University, USA)
    Abstract

    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.

    Short Bio

    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.

Coffee Break
Session 2
  • Bridging Hardware and Software Formal Verification for Reliable Computing Systems (PDF)
    Speaker:
    Nian-Ze Lee (LMU Munich, Germany)
  • Dynamic Cooperative Verification
    Speaker:
    Marek Chalupa (ISTA, Austria)
  • Dynamic Program Splitting enables Cooperation between Off-the-Shelf Verifiers
    Speaker:
    Cedric Richter (University of Oldenburg, Germany)
  • Integrating Deductive Program Verification, Bounded Model Checking, and Type Checking: The Karlsruhe Java Verification Suite
    Speaker:
    Bernhard Beckert (KIT, Germany)
Lunch
Session 3
  • Towards Cooperative Verification with Large Language Models
    Speaker:
    Christian Jan├čen (University of Oldenburg, Germany)
  • Towards Algorithm Selection for Test-Case Generation with CPAchecker (PDF)
    Speaker:
    Marie-Christine Jakobs (LMU Munich, Germany)
  • Race Witnesses and Cooperative Data Race Analysis with CoOpeRace
    Speaker:
    Vesal Vojdani (University of Tartu, Estonia)
  • LIV: Loop-Invariant Validation using Straight-Line Programs
    Speaker:
    Marian Lingsch-Rosenfeld (LMU Munich, Germany)
Coffee Break
Session 4
  • Common Framework for Transformation of Safety and Liveness Properties to ReachSafety
    Speaker:
    Marek Jankola (LMU Munich, Germany)
  • CPADaemon: Mitigating Tool Restarts for Java Verifiers
    Speaker:
    Henrik Wachowitz (LMU Munich, Germany)
  • Discussion and Closing
    Speaker:
    Dirk Beyer (LMU Munich, Germany) and Heike Wehrheim (University of Oldenburg, Germany)