verification

Klever automates static verification of GNU C industrial systems such as Linux kernel code against a variety of requirements. It employs software model checkers, primarily CPAchecker, to find memory safety errors, data races, and incorrect API usage, that are hard to detect otherwise.