Program

Workshop Program, November 14

10:00 - 10:10: Opening (Cyrille Artho and Peter Csaba Ölveczky)

10:10 - 11:00: Specification and verification (chair: Étienne André)

• Pedro Gomes, Dilian Gurov and Marieke Huisman:
  Specification and Verification of Synchronization with Condition Variables
• Brijesh Dongol:
  An interval logic for stream-processing functions: A convolution-based construction

11:00-11:30: Coffee break

11:30-12:20: Automotive and railway systems (chair: Osman Hasan)

• Shuichi Sato, Shogo Hattori, Hiroyuki Seki, Yutaka Inamori and Shoji Yuen:
  Automating Time Series Safety Analysis for Automotive Control Systems in STPA using Weighted Partial Max-SMT
• Eduard Kamburjan and Reiner Hähnle:
  Uniform Modeling of Railway Operations

12:20-13:30: Lunch

13:30-15:20: Invited talk + Security, Internet of things (chair: Cyrille Artho)

• Invited talk: Naoki Kobayashi
  On Two Higher-Order Extensions of Model Checking
• Imran Abbasi, Faiq Khalid Lodhi, Awais Kamboh and Osman Hasan:
  Formal Verification of Gate-Level Multiple Side Channel Parameters to detect Hardware Trojans
• Maissa Elleuch, Osman Hasan, Sofiene Tahar and Mohamed Abid:
  Formal Probabilistic Analysis of a WSN-based Monitoring Framework for IoT Applications

15:20-15:50: Coffee break

15:50-17:05: Cyber-physical systems and parameterized verification (chair: Sofiène Tahar)

• Richard Banach and Huibiao Zhu:
  Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems
• Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier Roux, Didier Lime and Étienne André:
  Applying parametric model-checking techniques for reusing real-time critical systems
• Nils Timm and Stefan Gruner:
  Parameterised Verification of Stabilisation Properties via Conditional Spotlight Abstraction

17:05-17:20: Closing