Process Algebra in PVS
Twan Basten and
Jozef Hooman
Computing Science Reports, Report 98-10,
Department of Computing Science, Eindhoven University of Technology,
1998, pp. 17.
Appeared in: Proceedings TACAS'99,
LNCS 1579,
Springer-Verlag, pages 270-284, 1999.
ABSTRACT
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.
Postscript Report 98-10
--
Postscript TACAS'99
© Springer-Verlag
Transparances TACAS'99 --
Dump file of all PVS theories