Download: PDF.
“Invariant inference for static checking: An empirical evaluation” by Jeremy W. Nimmer and Michael D. Ernst. In FSE 2002, Proceedings of the ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering, (Charleston, SC), Nov. 2002, pp. 11-20.
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, 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.
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.
Our observations not only provide a critical evaluation of these two techniques, but also highlight important considerations for creating future assistance tools.
Download: PDF.
BibTeX entry:
@inproceedings{NimmerE02:FSE,
author = {Jeremy W. Nimmer and Michael D. Ernst},
title = {Invariant inference for static checking: An empirical evaluation},
booktitle = {FSE 2002, Proceedings of the {ACM} {SIGSOFT} 10th
International Symposium on the Foundations of Software
Engineering},
pages = {11--20},
address = {Charleston, SC},
month = nov,
year = {2002}
}