Searching for a Solution to Program Verification=Equation Solving in CCS

Unique Fixpoint Induction, UFI, is a chief inference rule to prove the equivalence of recursive processes in CCS [7]. It plays a major role in the equational approach to verification. This approach is of special interest as it offers theoretical advantages in the analysis of systems that communicate values, have infinite state space or show parameterised behaviour. The use of UFI, however, has been neglected, because automating theorem proving in this context is an extremely difficult task. The key problem with guiding the use of this rule is that we need to know fully the state space of the processes under consideration. Unfortunately, this is not always possible, because these processes may contain recursive symbols, parameters, and so on. We introduce a method to automate the use of UFI. The method uses middle-out reasoning and, so, is able to apply the rule even without elaborating the details of the application. The method introduces variables to represent those bits of the proces...

• Type: Conference
• Year: 2000
• Where: MICAI
• Authors: Raul Monroy, Alan Bundy, Ian Green
• Keywords: Artificial Intelligence, Chief Inference Rule, MICAI 2000, State Space, Unique Fixpoint Induction