Refining Alloy-Based Mutation Operators to Reflect Common Mistakes
This program is tentative and subject to change.
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 AprDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mTalk | 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 30mTalk | Verifying Multiple TLA+ Configurations with Blast Research Track | ||
15:00 30mTalk | Typestates Specification and Verification in Frama-C Research Track Sébastien Patte Université Paris-Saclay, CEA, List, Virgile Prevosto Université Paris-Saclay, CEA, List |