This verification example demonstrates a layered verification approach, where the functional properties of the program are verified via history-based reasoning (that is, recording the changes to a certain shared states as a process algebra).
Path to example file
Lines of code
318 lines (comments not included)
Lines of specification
96 lines (30.19% of the total)
Note, verification may take a while and has a time-out of 20 seconds.