Soundness and Completeness of the NRB Verification Logic
Logic in Computer Science
2018-09-06 v2
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.
Keywords
Cite
@article{arxiv.1306.5585,
title = {Soundness and Completeness of the NRB Verification Logic},
author = {Peter T. Breuer and Simon J. Pickin},
journal= {arXiv preprint arXiv:1306.5585},
year = {2018}
}
Comments
To appear in OpenCert 2013 Workshop, Sept 23, Madrid, 15p