Single-threaded incrementing

Several methods to increment a shared variable `val`, some of which verify and some do not (due to wrong/incomplete specification).

General Information

  • Backend: Silicon
  • Language: Java
  • Features: Loop invariants
  • Path to Example File: permissions/Incr.java
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 42 (comments not included)
  • Lines of Specification: 10 (23.8% of total)
  • Computation Time: 8.6 seconds