Invariants and atomics

This is a example verification case with atomic blocks and resource invariants, in the style of CSL. This file contains several methods, some of which verify and some not.

General information

ID117
Articlenone
Back-endSilicon
LanguagePVL
FeaturesAtomics, Statically-scoped locking
Sources
Path to example fileparallel/inv-test.pvl
Date2017-06-20

Statistical information

Lines of code55 lines (comments not included)
Lines of specification9 lines (16.36% of the total)
Computation time23064 milliseconds

Example code

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