Klever

Contributor Finished

Software verification framework for automated checking of industrial GNU C systems against a wide range of requirements.

Code

Klever is a successor of the Linux Driver Verification (LDV) Tools, extending the original platform toward broader industrial use cases and more flexible verification workflows.

My contributions focused primarily on experimental features and infrastructure improvements, many of which later informed or were reimplemented in CVV.

Key contributions:

  • Fixed multiple functional and performance-related bugs, improving overall efficiency.
  • Enabled detection of multiple errors by default, including memory safety property.
  • Updated and maintained platform support for verification of newer Linux kernel versions.