Alias and Change Calculi, Applied to Frame Inference

Alexander Kogtenkov, Bertrand Meyer, Sergey Velder

Alias analysis, which determines whether two expressions in a program may reference to the same object, has many potential applications in program construction and verification. We…