Relaxed prefix

Verification challenge from the VerifyThis competition: checking whether some given pattern is a _relaxed prefix_ if a given array. With being a _relaxed prefix_ we mean being a prefix when removing at most one element (from the pattern).

General Information

  • Backend: Silicon
  • Language: PVL
  • Features: Loop invariants, Quantified permissions
  • Path to Example File: verifythis/prefix.pvl
  • Should Verify: Yes
  • Date: 2017-06-21
  • Lines of Code: 43 (comments not included)
  • Lines of Specification: 18 (41.9% of total)