Longest common prefix
Verification challenge from VerifyThis: finding the least-common prefix of an array starting from two given indices.
|Features||Arrays, Loop invariants, Quantified permissions|
|Sources||VerifyThis competition 2012|
|Path to example file||verifythis/lcp.pvl|
|Lines of code||25 lines (comments not included)|
|Lines of specification||13 lines (52% of the total)|
Note, verification may take a while and has a time-out of 20 seconds.