The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.10 - October (1995 vol.21)
pp: 822-833
ABSTRACT
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.
INDEX TERMS
Software verification, theorem proving, logic synthesis, weak division, hardware verification.
CITATION
Mark Aagaard, Miriam Leeser, "Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification", IEEE Transactions on Software Engineering, vol.21, no. 10, pp. 822-833, October 1995, doi:10.1109/32.469458
14 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool