todo
For an alternative approach, see hehner:vstte:2008 and tuerk:vstte:2010.
Notes related to Loop invariant
Invariants, Modular verification
Papers related to Loop invariant
- Behavioral interface specification languages [hatcliff:compsurv:2012]
- Specified blocks [hehner:vstte:2008]
- A data driven approach for algebraic loop invariants [sharma:pls:2013]
- Local reasoning about while-loops [tuerk:vstte:2010]