Simple model abstraction

Very simple verification example with model-based abstraction. A process algebraic model is created that is able to perform a single action: "step", which increments some shared variable by one. We verify that this is a valid abstraction of a program that increases some shared value by one.

General Information

  • Backend: Silicon
  • Language: PVL
  • Features: Futures
  • Path to Example File: futures/TestFuture.pvl
  • Should Verify: Yes
  • Date: 2017-06-16
  • Lines of Code: 57 (comments not included)
  • Lines of Specification: 20 (35.1% of total)
  • Computation Time: 24.8 seconds