Challenge two of the VerifyThis2018 competition: verifying a combinatorial problem based on Project Euler problem #114. This algorithm calculates the total number of 'valid' sequences of black and white tiles of length 50, where a sequence is defined to be 'valid' if it does not contain a sequence of red tiles shorter than length 3.

General information

ArticleFTfJP 2018: An Exercise in Verifying Sequential Programs with VerCors
FeaturesArrays, Iteration contracts, Loop invariants, Quantified permissions, Sequences
SourcesVerifyThis competition 2018
Path to example fileverifythis2018/challenge2.pvl

Statistical information

Lines of code199 lines (comments not included)
Lines of specification156 lines (78.39% of the total)
Computation timeunknown

Example code

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