Hoare logic and VDM : machine-checked soundness and completeness proofs
Investigating soundness and completeness of verification calculi for imperative programming languages is a challenging task. Many incorrect results have been published in the past. We take advantage of the computer-aided proof tool LEGO to interactively establish soundness and completeness of both H...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
University of Edinburgh
1998
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561721 |