The University of Edinburgh -
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
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.

[Search These Pages] [DAI Home Page] [Comment]