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

ID159
Articlenone
Back-endSilicon
LanguagePVL
FeaturesLoop invariants, Quantified permissions
SourcesVerifyThis competition 2015
Path to example fileverifythis/prefix.pvl
Date2017-06-21

Statistical information

Lines of code43 lines (comments not included)
Lines of specification18 lines (41.86% of the total)
Computation timeunknown

Example code

Note, verification may take a while and has a time-out of 20 seconds.