Parameter reference immutability: Formal definition, inference tool, and comparison

Download: PDF, slides (PDF), slides (PowerPoint).

“Parameter reference immutability: Formal definition, inference tool, and comparison” by Shay Artzi, Jaime Quinonez, Adam Kieżun, and Michael D. Ernst. Automated Software Engineering, vol. 16, no. 1, Mar. 2009, pp. 145-192.
A previous version appeared as “Combined static and dynamic mutability analysis” by Shay Artzi, Adam Kieżun, David Glasser, and Michael D. Ernst. In ASE 2007: Proceedings of the 22nd Annual International Conference on Automated Software Engineering, (Atlanta, GA, USA), Nov. 2007, pp. 104-113.
A previous version appeared as “Combined static and dynamic mutability analysis” by Shay Artzi, Adam Kieżun, David Glasser, and Michael D. Ernst. MIT Computer Science and Artificial Intelligence Laboratory technical report MIT-CSAIL-TR-2007-020, (Cambridge, MA), March 23, 2007.
A previous version appeared as “Combined static and dynamic mutability analysis” by Shay Artzi, Michael D. Ernst, David Glasser, and Adam Kieżun. MIT Computer Science and Artificial Intelligence Laboratory technical report MIT-CSAIL-TR-2006-065, (Cambridge, MA), September 18, 2006.

Abstract

Knowing which method parameters may be mutated during a method's execution is useful for many software engineering tasks. A parameter reference is immutable if it cannot be used to modify the state of its referent object during the method's execution. We formally define this notion, in a core object-oriented language. Having the formal definition enables determining correctness and accuracy of tools approximating this definition and unbiased comparison of analyses and tools that approximate similar definitions.

We present Pidasa, a tool for classifying parameter reference immutability. Pidasa combines several lightweight, scalable analyses in stages, with each stage refining the overall result. The resulting analysis is scalable and combines the strengths of its component analyses. As one of the component analyses, we present a novel dynamic mutability analysis and show how its results can be improved by random input generation. Experimental results on programs of up to 185 kLOC show that, compared to previous approaches, Pidasa increases both run-time performance and overall accuracy of immutability inference.

Download: PDF, slides (PDF), slides (PowerPoint).

BibTeX entry:

@article{ArtziQKE2009,
   author = {Shay Artzi and Jaime Quinonez and Adam Kie{\.z}un and Michael
	D. Ernst},
   title = {Parameter reference immutability: Formal definition, inference
	tool, and comparison},
   journal = {Automated Software Engineering},
   volume = {16},
   number = {1},
   pages = {145--192},
   month = mar,
   year = {2009}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.