Refining Alloy-Based Mutation Operators to Reflect Common Mistakes

Alloy is a declarative modeling language that is wellsuited 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 introduces 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 users might make.