Abstract Invariant Inference for Static Checking:

Static checking can verify the absence of errors in a program, but often requires written annotations or specifications. As a result, static checking can be difficult to use effectively: it can be difficult to determine a specification and tedious to annotate programs. Automated tools that aid the annotation process can decrease the cost of static checking and enable it to be more widely used. This paper describes an evaluation of the effectiveness of two techniques to assist the annotation process: inference via static analysis and inference via dynamic invariant detection. We quantitatively and qualitatively evaluate 33 users in a program verification task over three small programs, using ESC/Java as the static checker, Houdini for static inference, and Daikon for dynamic detection. With a well-constructed test suite, Daikon produces fully-verifiable annotations; therefore, we supplied Daikon with poor test suites to study its effectiveness in suboptimal circumstances. Statistically significant results show that Daikon enables users to express more correct invariants; Houdini users do not take full advantage its capabilities; and both tools improve task completion. Interviews suggest that beginning users found Daikon to be helpful; Houdini to be neutral; static checking to be of potential practical use; and both assistance tools to have benefits. 1