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: permissions/RosterFixed.java