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).
Loop invariants, Quantified permissions
VerifyThis competition 2015
Path to example file
Lines of code
43 lines (comments not included)
Lines of specification
18 lines (41.86% of the total)
Note, verification may take a while and has a time-out of 20 seconds.