Abstract
PAM is a general proof tool for process algebras. It allows users to define their own calculi and then perform algebraic style proofs in these calculi by directly manipulating process terms. The logic that PAM implements is equational logic plus recursion, with some features tailored to the particular requirements of process algebras. Equational reasoning is implemented by rewriting, while recursion is dealt with by induction. Proofs are constructed interactively, giving users the freedom to control the proof processes.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bergstra, J.A., Klop, J.W., “Process Theory Based on Bisimulation Semantics”, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 1989.
Boudol, G., Roy, V., de Simone, R., Vergamini, D., Process Calculi, From Theory to Practice: Verification Tools, INRIA Report No 1098, 1989.
Cleaveland, R., Parrow, J. and Steffen, B., “The Concurrency Workbench”, Proc. of the Workshop on Automated Verification Methods for Finite State Systems, LNCS 407, 1989.
Dershowitz, N., Jouannaud, J.-P., “Rewrite Systems”, in Handbook of Theoretical Computer Science North-Holland, 1989.
Godskesen, J.C., Larsen, K.G., Zeeberg, M., TAV Users Manual, Internal Report, Aalborg University Centre, Denmark, 1989.
Hennessy, M., Algebraic Theory of Processes, MIT Press, 1988.
Mauw, S., Veltink, G.J., A proof Asisteant for PSF. Programming Research Group, University of Amsterdam, 1991. In this Volume.
Hoare, C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985.
Milner, R., Concurrency and Communication, Prentice-Hall, 1989.
De Nicola, R., Inverardi, P., Nesi, M., “Using the Axiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications”, Proc. Workshop on Automatic Verification Methods for finite State Systems, LNCS 407, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lin, H. (1992). PAM: A process algebra manipulator. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_14
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive