Soundness and Completeness of the NRB Verification Logic

TL;DR

This paper presents a model and proof of completeness for the NRB verification logic, which is used for automated semantic checks of large C codebases like the Linux kernel, ensuring all potential defect triggers are caught.

Contribution

It introduces a colored state transitions model that approximates program behavior and proves the logic's soundness and completeness for deterministic imperative programs.

Findings

The model accurately captures possible program transitions.

The logic detects all defect-triggering traces, with some false positives.

Provides theoretical foundation for automated code verification.

Abstract

This short paper gives a model for and a proof of completeness of the NRB verification logic for deterministic imperative programs, the logic having been used in the past as the basis for automated semantic checks of large, fast-changing, open source C code archives, such as that of the Linux kernel source. The model is a colored state transitions model that approximates from above the set of transitions possible for a program. Correspondingly, the logic catches all traces that may trigger a particular defect at a given point in the program, but may also flag false positives.