Formalization of Correct Usage of Kernel Core API

by Denis for The Linux Foundation

Linux Driver Verification (LDV) program is devoted to developing an integrated framework for device drivers verification and adopting leading edge research results to enhance quality of verification tools. Currently LDV tools are used to check Linux device drivers against several safety rules, each of them formally defines what is correct usage of a particular part of kernel core API. This project is aimed at extending number of rules supported by the framework.