Klever: Verification Framework for Critical Industrial C Programs

TL;DR

Klever is a verification framework that streamlines the application of automatic software verification tools to large, critical industrial C programs, addressing scalability and usability challenges.

Contribution

It introduces a comprehensive framework that simplifies environment modeling, requirement specification, and verification across multiple program versions for industrial C software.

Findings

Reduces verification effort for large industrial programs

Supports verification of multiple program configurations

Enhances assessment of verification results

Abstract

Automatic software verification tools help to find hard-to-detect faults in programs checked against specified requirements non-interactively. Besides, they can prove program correctness formally under certain assumptions. These capabilities are vital for verification of critical industrial programs like operating system kernels and embedded software. However, such programs can contain hundreds or thousands of KLOC that prevent obtaining valuable verification results in any reasonable time when checking non-trivial requirements. Also, existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results. In this paper, we present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs.