This directory contains CIVL's solution for the challenge 1 of
VerifyThis 2017 Competition.  Detailed description of challenge 1 can
be found in :
"https://www.ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/challenge1.pdf"

The sorted and permutation properties of the original Java code is
verified with bounds : "civl verify challenge1-short.cvl"

The original Java code was modified for side-effect removing and its
sorted property is verified without bound : "civl verify -loop
pairInsertSort.cvl"