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...

• Type: Conference
• Year: 2002
• Where: SIGSOFT
• Authors: Jeremy W. Nimmer, Michael D. Ernst
• Keywords: Daikon Enables Users, SIGSOFT 2002, Software Engineering, Static Checking, Static Inference