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

This program is tentative and subject to change.

Mon 28 Apr 2025 14:00 - 14:30 at 203 - Session 5 - Formal Specification and Verification:

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well-suited for verifying system designs. A key strength of Alloy is its scenario-finding toolset, the Analyzer, which allows users to explore all valid scenarios that adhere to the model’s constraints up to a user-provided scope. Despite the Analyzer, writing correct Alloy models remains a difficult task, partly due to Alloy’s expressive operators, which allow for succinct formulations of complex properties but can be difficult to reason over manually. One recent body of work introduced mutation testing for Alloy models, that can also automatically generate a mutant-killing test suite. Unfortunately, a recent empirical study highlights that the existing first order mutant operators are not reflective of common mistakes. Therefore, this paper explores ways in which we can augment the mutation testing process to generate mutants that better reflect actual mistakes that could be made.

This program is tentative and subject to change.

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
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
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