Verification of a string to integer conversion program

Deductive verification of a string to integer conversion program kstrtoul in Linux OS kernel library is described. The kstrtoul program calculates the integer value presented as a char sequence of digits. To simplify program verification the transformations of replacing pointer operators to equivalent actions without pointers are conducted. Model of inner program state are constructed to enhance program specification. Deductive verification was conducted in the tools Why3 and Coq.