Parallel Block: Blanking

Simple verification example case where multiple sorts of data structures are "blanked" (that is, `0` is assigned to each element); first a single variable, then an array, and finally a matrix. All three sorts are connected via consecutive parallel blocks.

General Information

  • Backend: Silicon
  • Language: PVL
  • Features: Iteration contracts, Arrays, Matrices, Statically-scoped parallelism, Quantified permissions
  • Path to Example File: parallel/zero-many.pvl
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 36 (comments not included)
  • Lines of Specification: 17 (47.2% of total)
  • Computation Time: 53.4 seconds