MutDafny: A Mutation-Based Approach to Assess Dafny Specifications

TL;DR

MutDafny employs mutation testing to identify weaknesses in Dafny specifications, enhancing their reliability by detecting potential flaws through automated fault injection and verification.

Contribution

This paper introduces MutDafny, a novel mutation-based tool that automatically signals weaknesses in Dafny specifications, including new mutation operators tailored for Dafny.

Findings

MutDafny identified five weak specifications in real-world Dafny programs.

The tool used 40 mutation operators, combining existing and new Dafny-specific ones.

Evaluation on 794 programs demonstrated its effectiveness in revealing specification flaws.

Abstract

In verification-aware languages, such as Dafny, despite their critical role, specifications are as prone to error as implementations. Flaws in specifications can result in formally verified programs that deviate from the intended behavior. In this paper, we explore the use of mutation testing to reveal weaknesses in formal specifications written in Dafny. We present MutDafny, a tool that increases the reliability of Dafny specifications by automatically signaling potential weaknesses. Using a mutation testing approach, we introduce faults (mutations) into the code and rely on formal specifications for detecting them. If a program with a mutant verifies, this may indicate a weakness in the specification. We extensively analyze mutation operators from popular tools, identifying the ones applicable to Dafny. In addition, we synthesize new operators tailored for the language from bugfix commits in publicly available Dafny projects on GitHub. Drawing from both, we equipped our tool with a total of 40 mutation operators. We evaluate MutDafny's effectiveness and efficiency on a dataset of 794 real-world Dafny programs, and manually analyze a subset of the resulting undetected mutants, identifying five weak real-world specifications (on average, one at every 241 lines of code) that would benefit from strengthening.