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 seed for a comprehensive solution to the "frame problem" and as an alternative (for the specific issue of determining aliases) to separation logic, shape analysis, ownership types and dynamic frames.
Bertrand Meyer. Steps Towards a Theory and Calculus of Aliasing. International Journal of Software and Informatics, 2011,5(1-2Part1):77~115Copy