2 September 2020

  • 12:00 – 13:00: Social lunch + CONCUR Test-of-Time award
  • 13:00 – 13:55: FMICS Keynote
    • Stefan Resch: Applying Formal Methods in Industrial Railway Applications at Thales
  • 13:55 – 14:15: Thierry Lecomte, Bruno Lavaud, Lilian Burdy and Denis Sabatier: A Safety Flasher Developed with the CLEARSY Safety Platform
  • 14:15 – 14:45: breakout
  • 14:45 – 16:00: Session “Temporal Logic and Model checking”
    • 14:45 – 15:10: Olav Bunte, Tim A.C. Willemse and Louis C.M. van Gool: Formal verification of OIL component specifications using mCRL2
    • 15:10 – 15:35: Samuel Huang and Rance Cleaveland: Temporal Logic Query Checking over Finite Data Streams
    • 15:35 – 16:00: Umar Ozeer, Gwen Salaün, Loic Letondeur, Francois-Gael Ottogalli and Jean-Marc Vincent: Verification of a Failure Management Protocol for Stateful IoT Applications
  • 16:00 – 16:30: breakout
  • 16:30 – 17:30: CONCUR + QEST + FMICS Keynote
    • Thomas Henzinger: A Survey of Bidding Games on Graphs
  • 17:30 – 17:45: breakout
  • 17:45 – 19:00: Session “Formal Verification and Security Analysis”
    • 17:45 – 18:10: Qingmei Wu, Nathan Fulton and Jessie Rosenberg: A Formally Verified Plasma Vertical Position Control Algorithm
    • 18:10 – 18:35: Yanni Kouskoulas, Tj Machado and Daniel Genin: Formally Verified Timing Computation for Non-deterministic Horizontal Turns During Aircraft Collision Avoidance Maneuvers
    • 18:35 – 19:00: Fereidoun Moradi, Sara Abbaspour Asadollah, Ali Sedaghatbaf, Aida Causevic, Marjan Sirjani and Carolyn Talcott: An Actor-based Approach for Security Analysis of Cyber-Physical Systems

3 September 2020

  • 12:00 – 13:00: Social lunch + FMICS Best Paper Award + Sponsorship
  • 13:00 – 14:15: Session “Quantitative Analysis and Cyber-Physical Systems”
    • 13:00 – 13:25: Rong Gu, Eduard Enoiu, Cristina Seceleanu and Kristina Lundqvist: Verifiable and Scalable Mission-Plan Synthesis for Multiple Autonomous Agents
    • 13:25 – 13:50: Markus Klinik, Bernard van Gastel, Cynthia Kop and Marko Van Eekelen: Skylines for Symbolic Energy Consumption Analysis
    • 13:50 – 14:15: Benjamin Binder, Mihail Asavoae, Florian Brandner, Belgacem Ben Hedia and Mathieu Jan: Scalable Detection of Amplification Timing Anomalies for the Superscalar TriCore Architecture
  • 14:15 – 14:45: breakout
  • 14:45 – 15:05: Michael Butler, Philipp Koerner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia and Laurent Voisin: The First Twenty-Five Years of Industrial Use of the B Method
  • 15:05 – 16:00: FMICS 25th Birthday Festivities:
    • “Formal Methods for Industrial Critical Systems – Genesis, Success Stories, and the Next 25 Years” (panel)
  • 16:00 – 16:30: breakout
  • 16:30 – 17:30: CONCUR + FORMATS + FMICS Keynote
    • Roderick Bloem: Safe Reinforcement Learning using Probabilistic Shields