Plaisted, David Programming Logics, MPI for Informatics, Max Planck Society;
Chadha, R., & Plaisted, D. (1993). On the Mechanical Derivation of Loop Invariants. Journal of Symbolic Computation, 15(5/6), 705-744.