A failing verification case in which the correctness of processes and axioms is checked, in the context of history-based reasoning. Currently this example does not verify due to refactoring of VerCors.
Path to example file
Lines of code
51 lines (comments not included)
Lines of specification
15 lines (29.41% of the total)
Note, verification may take a while and has a time-out of 20 seconds.