Longest common prefix

Verification challenge from VerifyThis: finding the least-common prefix of an array starting from two given indices.

General information

ID158
Articlenone
Back-endSilicon
LanguagePVL
FeaturesArrays, Loop invariants, Quantified permissions
SourcesVerifyThis competition 2012
Path to example fileverifythis/lcp.pvl
Date2017-06-21

Statistical information

Lines of code25 lines (comments not included)
Lines of specification13 lines (52% of the total)
Computation timeunknown

Example code

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