Alias calculus for a simple imperative language with decidable pointer arithmetic

Alias calculus was proposed by Bertrand Meyer in 2011 for a toy programming language with a single data type for abstract pointers. This original calculus is a set-based formalism insensitive to the control flow; it is a set of syntaxdriven rules how to compute an upper approximation aft(S, P) for aliasing after the execution of a program P for a given initial aliasing S. The primary purpose of our paper is to present a variant of alias calculus for a more realistic programming language with automatic and dynamic memory, regular data and a decidable pointer arithmetic. Our variant is insensitive to the control flow (like the original calculus by B. Meyer), but (in contrast to the original calculus) this calculus is equation-based.