Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: A Theorem Proving Based Methodology for Software Verification
Authors: Aagaard, Mark
Leeser, Miriam
Keywords: computer science
technical report
Issue Date: Mar-1993
Publisher: Cornell University
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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
93-1335.pdf4.55 MBAdobe PDFView/Open
93-1335.ps1 MBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us