Abstract
A simple semantic model for the NRB logic of program verification is provided here, and the logic is shown to be sound and complete with respect to it. That provides guarantees in support of the logic's use in the automated verification of large imperative code bases, such as the Linux kernel source. 'Soundness' implies that no breaches of safety conditions are missed, and 'completeness' implies that symbolic reasoning is as powerful as model-checking here. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Breuer, P. T., & Pickin, S. J. (2014). Soundness and completeness of the NRB verification logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8368 LNCS, pp. 389–404). Springer Verlag. https://doi.org/10.1007/978-3-319-05032-4_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
