A survey of loop invariants - Carlo A. Furia; Bertrand Meyer 001; Sergey Velder (CoRR, 2012)

Alias and Change Calculi, Applied to Frame Inference. - Alexander Kogtenkov; Bertrand Meyer 001; Sergey Velder (CoRR, 2013)

Loop invariants: Analysis, classification, and examples. - Carlo A. Furia; Bertrand Meyer 001; Sergey Velder (ACM Comput. Surv., 2014)

Alias calculus, change calculus and frame inference. - Alexander Kogtenkov; Bertrand Meyer 001; Sergey Velder (Sci. Comput. Program., 2015)