FormaliSE 2025
Sun 27 - Mon 28 April 2025 Ottawa, Ontario, Canada
co-located with ICSE 2025
Mon 28 Apr 2025 14:30 - 15:00 at 203 - Session 5 - Formal Specification and Verification: Chair(s): Toshiaki Aoki

TLA+ is one of the most popular formal methods for designing concurrent and distributed systems. TLA+ specifications can be verified with the TLC model-checker, but unfortunately only one user-specified configuration of the system is verified at once. If configurations are simple (e.g. the number of processes in a concurrent algorithm) it is viable to run TLC for several configurations to gain confidence that the system indeed works correctly for all of them. However, for complex configurations it is difficult to do so, and critical configurations can easily be missed. This paper introduces Blast, a tool that simplifies this task, by enabling the user to easily verify a TLA+ specification for all configurations inside a given scope. Our evaluation using a large benchmark of TLA+ examples, shows that Blast can be effectively used in a wide range of specifications and helped us uncover issues in several of them.

Mon 28 Apr

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

14:00 - 15:30
Session 5 - Formal Specification and Verification:Research Track at 203
Chair(s): Toshiaki Aoki JAIST
14:00
30m
Talk
Refining Alloy-Based Mutation Operators to Reflect Common Mistakes
Research Track
Ana Jovanovic The University of Texas at Arlington, Mohammad Nurullah Patwary The University of Texas at Arlington, Allison Sullivan University of Texas at Arlington
14:30
30m
Talk
Verifying Multiple TLA+ Configurations with Blast
Research Track
Paul Somson INESC TEC, Alcino Cunha University of Minho; INESC TEC
Pre-print
15:00
30m
Talk
Typestates Specification and Verification in Frama-C
Research Track
Sébastien Patte Université Paris-Saclay, CEA, List, Virgile Prevosto Université Paris-Saclay, CEA, List