History-based reasoning: correctness checking (PVL)

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.

General information

ID70
Articlenone
Back-endSilicon
LanguagePVL
FeaturesHistories
Sources
Path to example filehistories/History.pvl
Date2017-06-19

Statistical information

Lines of code51 lines (comments not included)
Lines of specification15 lines (29.41% of the total)
Computation time27045 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.