Report Number: CS-TR-79-740
Institution: Stanford University, Department of Computer Science
Title: The logic of aliasing
Author: Cartwright, Robert
Author: Oppen, Derek C.
Date: September 1979
Abstract: We give a new version of Hoare's logic which correctly handles programs with aliased variables. The central proof rules of the logic (procedure call and assignment) are proved sound and complete.
http://i.stanford.edu/pub/cstr/reports/cs/tr/79/740/CS-TR-79-740.pdf