Fork/join incrementing (failing 2)

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.

General information

ID155
Articlenone
Back-endSilicon
LanguageJava
FeaturesFork/join concurrency
Sources
Path to example filethreads/VerifiedMain-E2.java
Date2017-06-21

Statistical information

Lines of code13 lines (comments not included)
Lines of specification4 lines (30.77% of the total)
Computation timeunknown

Example code

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