FormaliSE 2025
Sun 27 - Mon 28 April 2025 Ottawa, Ontario, Canada
co-located with ICSE 2025

This program is tentative and subject to change.

Disasters are unexpected, and capable of severely impacting an urban region. A key challenge for disaster managers is to distribute resources to meet evolving demand. This paper presents a work in progress framework to verify provably correct team strategies to safely carry out resource distribution. Uncertainties from infrastructure damage and team fatigue are modelled using Markov Decision Processes, and verified against temporal logic properties to support disaster managers resourcing decisions. We implement the framework with PRISM and test it’s effectiveness across a range of resourcing scenarios.

This program is tentative and subject to change.

Sun 27 Apr

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
Session 2 – Theorem Proving and Probabilistic Model CheckingResearch Track at 203
14:00
30m
Talk
The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs
Research Track
Chengsong Tan Imperial College London, Kaihong, Alastair F. Donaldson Imperial College London, Jonathan Julian Huerta y Munive Czech Technical University, John Wickerson Imperial College London
14:30
30m
Talk
A proof-based ground algebraic meta-model for reasoning on ASTD in Event-B
Research Track
Christophe Chen INPT-ENSEEIHT/IRIT, Peter Rivière INPT-ENSEEIHT / IRIT, University of Toulouse, France, Neeraj Kumar Singh INPT-ENSEEIHT/IRIT, Guillaume Dupont INPT–ENSEEIHT, Yamine Ait Ameur IRIT/INPT-ENSEEIHT, Marc Frappier Université de Sherbrooke, Canada
15:00
30m
Talk
Probabilistic Model Checking of Disaster Resource Distribution Strategies
Research Track
Kenneth Johnson Auckland University of Technology, Meena Kumari Auckland University of Technology