Issue No. 10 - October (1995 vol. 21)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.469458
We describe the verification of a logic-synthesis tool with the Nuprl proof-development system. The logic-synthesis tool, <it>Pbs</it>, implements the weak-division algorithm. <it>Pbs</it> consists of approximately 1,000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high-level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of <it>Pbs</it> in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying <it>Pbs</it> we developed a consistent approach for using a proof-development system to reason about functional programs. The approach hides implementation details and uses higher-order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher-order proof system, and can aid in the future verification of large software implementations.
Software verification, theorem proving, logic synthesis, weak division, hardware verification.
M. Leeser and M. Aagaard, "Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification," in IEEE Transactions on Software Engineering, vol. 21, no. , pp. 822-833, 1995.