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

  • Backend: Silicon
  • Language: PVL
  • Features: Sequences, Iteration contracts, Arrays, Loop invariants, Quantified permissions
  • Path to Example File: verifythis2018/challenge2.pvl
  • Should Verify: Yes
  • Date: 2018-05-09
  • Lines of Code: 199 (comments not included)
  • Lines of Specification: 156 (78.4% of total)