Трансформация, спецификация и верификация программы вычисления числа элементов множества, представленного в виде битовой шкалы

Transformation, specification, and verification of the program calculating the elements number of a set presented by a bit vector

Article's language
Russian
Abstract
Transformations eliminating pointers in the memweight function in OS Linux kernel library is described. Next, the function is translated to the predicate programming language P. For the obtained predicate program, deductive verification in the Why3 tool was performed. In order to simplify verification, the program model of calculating program inner state was constructed.
UDK
Pages
103-136
File
Number