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

  • Backend: Silicon
  • Language: Java
  • Features: Fork/join concurrency
  • Path to Example File: threads/VerifiedMain-E2.java
  • Should Verify: Yes
  • Date: 2017-06-21
  • Lines of Code: 13 (comments not included)
  • Lines of Specification: 4 (30.8% of total)