Edinburgh Research Explorer

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Documents

Original languageEnglish
Title of host publicationMICAI 2000: Advances in Artificial Intelligence
Subtitle of host publicationMexican International Conference on Artificial Intelligence, Acapulco, Mexico, April 11-14, 2000. Proceedings
PublisherSpringer-Verlag GmbH
Pages1-12
ISBN (Electronic)978-3-540-45562-2
ISBN (Print)978-3-540-67354-5
DOIs
StatePublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume1793
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Abstract

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 behavior.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 processes’ state space that, at application time, were not known, hence, changing from equation verification to equation solving.Adding this method to the equation plan developed by Monroy, Bundy and Green [8], we have implemented an automated verification planner. This planner increases the number of verification problems that can be dealt with fully automatically, thus improving upon the current degree of automation in the field.

Download statistics

No data available

ID: 6322227