Invariant inference for static checking: An empirical evaluation
Submitted by mernst on Wed, 2011-11-30 14:35
| Title | Invariant inference for static checking: An empirical evaluation |
| Publication Type | Conference Paper |
| Year of Publication | 2002 |
| Authors | Nimmer JW, Ernst MD |
| Conference Name | Proceedings of the ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering (FSE 2002) |
| Date or Month Published | November 20–2 |
| Conference Location | Charleston, SC |
| Abstract | <p>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. </p> <p> This paper describes an evaluation of the effectiveness of two techniques, one static and one dynamic, to assist the annotation process. We quantitatively and qualitatively evaluate 41 programmers using ESC/Java in a program verification task over three small programs, using Houdini for static inference and Daikon for dynamic inference. We also investigate the effect of unsoundness in the dynamic analysis. </p> <p> Statistically significant results show that both inference tools improve task completion; Daikon enables users to express more correct invariants; unsoundness of the dynamic analysis is little hindrance to users; and users imperfectly exploit Houdini. Interviews indicate 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 unique benefits. </p> <p> Our observations not only provide a critical evaluation of these two techniques, but also highlight important considerations for creating future assistance tools.</p> |
| Downloads | PDF PostScript |
| Citation Key | NimmerE02:FSE |
Last changed Mon, 2013-06-03 10:27

cs.