Automatic proof of correctness of a binary addition algorithm
J Strother Moore · ACM SIGART Bulletin · 1975
The Boyer-Moore Pure LISP Theorem Prover ([1], [2], and [3]) has recently proved the correctness of a program implementing binary addition with a carry flag. Because of the relative complexity of the binary addition algorithm and the automatic nature of the proof, this result was thought interesting enough to warrant this technical note.