TRANSFORMATION, SPECIFICATION, AND VERIFICATION OF THE PROGRAM CALCULATING THE ELEMENTS NUMBER OF A SET PRESENTED BY A BIT VECTOR
Erdem Tumurov, Vladimir Ivanovich Shelekhov · System Informatics · 2020
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.