Automatic program verification V: verification-oriented proof rules for arrays, records and pointers

purl.stanford.edu/kb470yn0165