Program

The conference programm is cordinated with CONFEST 2025:

Wednesday 27 August

Session 09:00-9:50 Invited talk
Ina Schieferdecker on Navigating the growing field of research on AI for software testing – the taxonomy for AI-augmented software testing and an ontology-driven literature survey

Coffee Break 9:50-10:20

Session 10:20-12:00 on Verification

  • Hatcliff, John, Belt, Jason, Robby, FNU, McKenzie, Clint, Liang, Catalina: End-to-End Formal Methods Integrated Development with SysMLv2 using HAMR

  • Armborst, Lukas, Beyer, Dirk, Huisman, Marieke, Lingsch-Rosenfeld, Marian: AutoSV-Annotator: Integrating Deductive and Automatic Software Verification

  • van de Sand, Niklas, Völker, Marcus: IC3 for Loop Invariant Generation in Deductive Verification of Control Code

  • Baier, Christel, Klatt, Rio, Klüppelholz, Sascha, Lehmann, Johannes: Backward Responsibility in Transition Systems Beyond Safety

Lunch 12:00-13:30

Session 13:30-14:20 shared with Confest

Coffee Break 14:20-14:40

Session 14:40-15:55 Automotive and Railway

  • THOMÉ, Émilie, Tasson, Christine, DENIS, Xavier: GRust: A Programming Language for Automotive Engineering

  • Sequeira, Tiago, Pedro, André: Robust Spatio-Temporal Logic Semantics for Autonomous Driving Systems Falsification

  • Carnevali, Laura, Fantechi, Alessandro, Gori, Gloria, Vreshtazi, Denis, Borselli, Alessandro, Cefaloni, Maria Rosaria, Rota, Lucio : Data-Driven Synthesis of Stochastic Fault Trees for Proactive Maintenance of Railway Vehicles

Coffee Break 15:55-16:15

Session 16:15-17:30 Cyber-Physical Systems

  • Schaber, Felix, Mashkoor, Atif, Leuschel, Michael: Promise-Driven Modeling: A Structured Approach for Modeling Cyber- Physical Systems

  • Kröger, Janis, Stierand, Ingo, Fränzle, Martin: Ensuring Integration Conditions during the Update of Cyber-Physical Systems at Runtime

Thursday 28 August

Session 09:00-9:50 Program Verification

  • Beers, Adrian, Booy, Jore, Groote, Jan Friso, Bogaard, van den, Johan, Bouwman, Mark: A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier

  • Hallerstede, Stefan, Robby, FNU, Hatcliff, John, Belt, Jason, Hardin, David: Proof Engineering in Logika: Synergistically Integrating Automated and Semi-Automated Program Verification

Coffee Break 9:50-10:10

Session 10:10-11:00 Embedded Systems

  • Bonafini, Federico, Cavada, Roberto, Cimatti, Alessandro, Gomez, Guillermo, Tonetta, Stefano: A Specification-Driven Approach to Embedded FDIR Code Generation

  • Brandhøj, Andreas, Bøgedal, Tobias Worm, Rydhof Hansen, René, Larsen, Kim, Poulsen, Danny: Building a Modular Platform for Model Checking Glitch Attacks in RISC-V Programs

Coffee Break 11:00-11:20

Invited talk 11:20-12:10
Arnd Hartmanns on An Overview of Sound and Modest Approaches to Quantitative Model Checking from Sea to Space

Lunch 12:10-13:30

Business Meetings 13:30-14:30

Social Event + Dinner 15:30-21:00