Definite Reference Mutability
Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable references may not be truly mutable, but mutable due to approximation.
In this paper, we present ReM (for definite Re[ference] M[utability]). It separates potentially mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all potentially mutable references are definitely mutable.
Sat 21 Jul
11:00 - 12:40: ECOOP Research Papers - Static Analysis at Zurich II Chair(s): Karim AliUniversity of Alberta | ||||||||||||||||||||||||||||||||||||||||||
11:00 - 11:25 Research paper | DOI | |||||||||||||||||||||||||||||||||||||||||
11:25 - 11:50 Research paper | DOI Pre-print | |||||||||||||||||||||||||||||||||||||||||
11:50 - 12:15 Research paper | Ana MilanovaRensselaer Polytechnic Institute DOI | |||||||||||||||||||||||||||||||||||||||||
12:15 - 12:40 Research paper | Neville GrechUniversity of Athens, George KastrinisUniversity of Athens, Yannis SmaragdakisUniversity of Athens DOI |