Synthesis
Inferring loop invariants using post-conditions:http://se.ethz.ch/~meyer/publications/proofs/invariant_inference.pdf
Generating loop invariants using predicate abstraction
https://hal.inria.fr/inria-00615623/document
Boogie uses abstract interpretation to infer loop invariants:
http://research.microsoft.com/en-us/um/people/leino/papers/krml160.pdf
Tools
Boogie overview slidehttp://webcourse.cs.technion.ac.il/236800/Winter2010-2011/ho/WCFiles/Boogie.pdf
