Invariant inference for static checking: An empirical evaluation

Download: PDF, PostScript.

“Invariant inference for static checking: An empirical evaluation” by Jeremy W. Nimmer and Michael D. Ernst. In Proceedings of the ACM SIGSOFT 10th International Symposium on the Foundations of Software Engineering (FSE 2002), (Charleston, SC), November 20-22, 2002, pp. 11-20.
A revised version appeared as “Automatic Generation and Checking of Program Specifications” by Jeremy W. Nimmer. MIT Laboratory for Computer Science technical report 852, (Cambridge, MA), June 10, 2002. Revision of author's Master's thesis.
A revised version appeared as “Automatic Generation and Checking of Program Specifications” by Jeremy W. Nimmer. Masters thesis, MIT Department of Electrical Engineering and Computer Science, (Cambridge, MA), May 2002.

Abstract

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

BibTeX entry:

@inproceedings{NimmerE02:FSE,
   author = {Jeremy W. Nimmer and Michael D. Ernst},
   title = {Invariant inference for static checking: An empirical evaluation},
   booktitle = {Proceedings of the {ACM} {SIGSOFT} 10th International
	Symposium on the Foundations of Software Engineering (FSE 2002)},
   pages = {11--20},
   address = {Charleston, SC},
   month = {November~20--22,},
   year = {2002}
}

(This webpage was created with bibtex2web.)

Back to Program Analysis Group publications.