Steps towards a theory and calculus of aliasing
arXiv:1001.1610
Abstract
A theory, graphical notation, mathematical calculus and implementation for finding whether two given expressions can, at execution time, denote references attached to the same object. Intended as the basis for a comprehensive solution to the "frame problem" and as a complement to, or even a replacement for, separation logic, shape analysis, ownership types and dynamic frames.
Revision of original JOT paper. To appear in IJSI (International Journal of Software and Informatics) in 2011. The original title was: The theory and calculus of aliasing