The verification example on page 42 of Clement Hurlin's PhD thesis. The example is a linked list representing grades (in a Roster). The roster has functionality to upgrade grades. We verify that these functions are correct.
Path to example file
Lines of code
61 lines (comments not included)
Lines of specification
23 lines (37.7% of the total)
Note, verification may take a while and has a time-out of 20 seconds.