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.

翻译：自动软件验证工具能够非交互地检查程序是否满足特定需求，帮助发现难以检测的缺陷。此外，它们还能在某些假设下形式化地证明程序正确性。这些能力对于操作系统内核和嵌入式软件等关键工业程序的验证至关重要。然而，此类程序可能包含成百上千KLOC的代码量，当验证非平凡需求时，这会阻碍在合理时间内获得有价值的验证结果。同时，现有工具缺乏广泛采用的环境建模、需求规约、多版本多配置目标程序验证以及验证结果专家评估手段。本文提出Klever软件验证框架，旨在降低将自动软件验证工具应用于大型关键工业C程序的工作量。