Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #781 | |
|---|---|
| Title: | Proof Planning the Verification of Ccs Programs |
| Authors: | Monroy-Borja,R; Bundy,A; Ireland,A; Hesketh,J |
| Date: | Jan 1996 |
| Presented: | Submitted to CADE-13, 1996 |
| Keywords: | |
| Abstract: | The verification of CCS programs has often been characterised as an expensive, time-consuming, and error-prone task, where computer assistance is thought to be essential. Yet, existing theorem proving based frameworks, for the verification of programs using CCS, are not much use because of their poor level of automation. In this paper, we propose the use of proof plans as the chief mechanism for the automation of CCS program verification. We present a collection of proof plan methods that guide a proof plan formation for the verification of deterministic, and divergence-free CCS programs. The meta-level reasoning embedded in these methods takes full advantage of the operational interpretation of processes while outputting plan steps to the appropriate object-level representation. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}