Automatic Construction of Verification Generators from Hoare Logics
Mark Moriconi, Richard L. Schwartz · NASA Technical Reports Server (NASA) · 1983
A method for mechanically constructing verification condition generators from a useful class of Hoare logics is defined. Any verification condition generator constructed is shown to be sound and deduction complete with respect to the associated Hoare logic. The method was implemented.