Process algebra in PVS

T. Basten, J.J.M. Hooman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)


The aim of this work is to investigate mechanical support for process algebra, both for concrete applications and theoretical properties. Two approaches are presented using the verification system PVS. One approach declares process terms as an uninterpreted type and specifies equality on terms by axioms. This is convenient for concrete applications where the rewrite mechanisms of PVS can be exploited. For the verification of theoretical results, often induction principles are needed. They are provided by the second approach where process terms are defined as an abstract datatype with a separate equivalence relation.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems (Proceedings 5th International Conference, TACAS'99; he;d as part of ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999)
EditorsW.R. Cleaveland
Place of PublicationBerlin
ISBN (Print)3-540-65703-7
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Process algebra in PVS'. Together they form a unique fingerprint.

Cite this