LSB: Analysis & Fixing of Race Condition Warnings in the Linux Kernel

The task is to catch bugs due to race conditions in Linux Kernel 5.4 device drivers. A software verification framework called Klever automates the verification against a concurrency safety requirement specification. Using the Klever web interface, the generated error traces are analyzed and classified as false warnings or real bugs. In case of bugs, a bug fix patch is prepared and sent to the driver subsystem developers, or a bug report is sent. Causes of the false warnings are also determined to improve the tool's environment models.