Верификация программы преобразования строки в целое число

Описывается дедуктивная верификация программы kstrtoul на языке Си из библиотеки ОС Linux. Программа kstrtoul реализует вычисление целого числа, представленного в виде последовательности литер. Чтобы упростить верификацию, применяются трансформации замены операций с указателями эквивалентными действиями без указателей. Программа преобразуется на язык предикатного программирования. Конструируется модель внутреннего состояния программы как часть спецификации программы. Дедуктивная верификация проведена в системах Why3 и Coq.