Automatic Program Verification II : Verifying Programs by Algebraic and Logical Reduction. AIM-255

purl.stanford.edu/qn052qn0181