A Theorem Proving Based Methodology for Software Verification

Abstract

We have developed an effective methodology for using a proof development system to prove properties about functional programs. This methodology includes techniques such as hiding implementation details and using higher order theorems to structure proofs and aid in abstract reasoning. The methodology was discovered and refined while verifying a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, $Pbs$, implements the weak division algorithm. $Pbs$ consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation of a hardware synthesis tool. The program was verified by embedding the subset of SML in Nuprl and then verifying the correctness of the implementation of $Pbs$ in the Nuprl logic.