Loop invariant

[Google Scholar] [Wikipedia]

Papers: hehner:vstte:2008, tuerk:vstte:2010

todo

For an alternative approach, see hehner:vstte:2008 and tuerk:vstte:2010.


Modular verification