Using Mutations to Analyze Formal Specifications
Siraphob Phipathananunth · 2022
The result of a formal verification is only as good as the specifications. A key challenge in automated verification is therefore coming up with a strong specification. This is somewhat analogous to having a good test suite in software testing. A well-studied technique for improving and assessing a test suite is mutation testing. It is a method for systematically modifying the source code to determine whether the resulting “mutants” can be “caught” by the tests. This paper explores mutation verification, i.e., the use of mutations to strengthen and assess the quality of formal specifications used in a verification tool. We built a prototype for mutation verification—dubbed Gambit—and used it for an industrial tool that verifies smart contracts. Early results indicate that Gambit generates useful mutants that can provide valuable insights about the coverage of the specifications.