A new structural coverage criterion for dynamic detection of program invariants

Dynamic detection of program invariants is emerging as an important research area with many challenging problems. Generating suitable test cases that support accurate detection of program invariants is crucial to the dynamic approach of program invariant detection. In this paper, we propose a new structural coverage criterion called invariant-coverage criterion for dynamic detection of program invariants. We also show how the invariant-coverage criterion can be used to improve the accuracy of dynamically detected invariants. We first used the Daikon tool to report likely program invariants using the branch coverage and all definition-use pair coverage test suites for several programs. We then generated invariant-coverage suites for these likely invariants. When Daikon was run with the invariant-coverage suites, several spurious invariants reported earlier by the branch coverage and definition-use pair coverage test suites were removed from the reported invariants. Our approach also produced more meaningful invariants than randomly generated test suites.