Simple fork/join program where the forked thread increments a shared counter by one. We intend this verification example to fail, as we do not unfold the "postjoin" predicate that contains information on the shared state after the thread has been joined.
Path to example file
Lines of code
13 lines (comments not included)
Lines of specification
4 lines (30.77% of the total)
Note, verification may take a while and has a time-out of 20 seconds.