Abstract
A proof assistant for process algebras is described. The main novelty of this proof system is that it is parameterised by process calculi: the users can define their own calculi by providing suitable signatures and axioms. Proofs are constructed by directly manipulating process terms, and some forms of induction has been built-in to handle recursion.
This work has been supported by the Science and Engineering Research Council of UK and the ESPRIT II BRA project CONCUR.
This is a preview of subscription content, log in via an institution.
References
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.
Godskesen, J.C., Larsen, K.G., Zeeberg, M., TAV Users Manual, Internal Report, Aalborg University Centre, Denmark, 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). An interactive proof tool for process algebras. In: Finkel, A., Jantzen, M. (eds) STACS 92. STACS 1992. Lecture Notes in Computer Science, vol 577. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55210-3_223
Download citation
DOI: https://doi.org/10.1007/3-540-55210-3_223
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55210-9
Online ISBN: 978-3-540-46775-5
eBook Packages: Springer Book Archive