Proving correctness of a program that calculates the histogram of a part of some input matrix.
|Language||OpenMP for C|
|Features||Arrays, Iteration contracts, Matrices|
|Path to example file||carp/histogram-submatrix.c|
|Lines of code||48 lines (comments not included)|
|Lines of specification||25 lines (52.08% of the total)|
|Computation time||45346 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.