I have mentioned this paper before but as a draft. It has now been accepted by ACM’s Computing Surveys and is scheduled to appear in September 2014; the current text, revised from the previous version, is available .
Here is the abstract:
Software veriﬁcation has emerged as a key concern for ensuring the continued progress of information technology. Full veriﬁcation generally requires, as a crucial step, equipping each loop with a “loop invariant”. Beyond their role in veriﬁcation, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, ﬁnding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common ﬂavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs.
We performed a systematic identiﬁcation, validation, and classiﬁcation of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study,governing how invariants are derived from postconditions;it proposes a taxonomy of invariants according to these patterns, and presents its application to the algorithms reviewed. The discussion also shows the need for high-level speciﬁcations based on “domain theory”. It describes how the invariants and the corresponding algorithms have been mechanically veriﬁed using an automated program prover; the proof source ﬁles are available. The contributions also include suggestions for invariant inference and for model-based speciﬁcation.
 Carlo Furia, Bertrand Meyer and Sergey Velder: Loop invariants: Analysis, Classification and Examples, in ACM Computing Surveys, to appear in September 2014, preliminary text available here.