Automatic Alias Analysis and Frame Inference

Take two expressions e and f , denoting references (pointers), and a program location p. When an execution reaches p, can e and f ever be attached (i.e., point) to a single object? This is the aliasing problem, undecidable like anything else of interest in computer science, but for which we may nevertheless expect good enough solutions. Applications abound, from the general verification of object-oriented programs to frame analysis and even deadlock analysis. The lectures will describe various forms of the alias calculus and how it has been applied to addressing these problems, as part of an integrated program development and verification environment.