Soundness and Completeness of the NRB Verification Logic

Peter T. Breuer, Simon J. Pickin

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 ba…