TRANSFORMATION AND VERIFICATION OF THE OS PROGRAM SORTING DEVICES IN A COMPUTER BUS
Vladimir Ivanovich Shelekhov · System Informatics · 2021
The transformation and verification of the bus_sort_breadthfirst program, which belongs to the Linux OS kernel and implements sorting of devices are described. The C program is transformed into the cP language performing macros unfolding, structure changes, and elimination of pointers. Transformed program is translated into the WhyML functional language. For the received program, a specification is constructed. Deductive verification is carried out in the tool Why3.