An Experiment using Term Rewriting Techniques for Concurrency

Citation

Shankland C (1991) An Experiment using Term Rewriting Techniques for Concurrency. In: Peyton JS, Hutton G & Holst C (eds.) Functional Programming, Glasgow 1990: Proceedings of the 1990 Glasgow Workshop on Functional Programming 13–15 August 1990, Ullapool, Scotland. Workshops in Computing. 1990 Glasgow Workshop on Functional Programming, Ullapool, UK, 13.08.1990-15.08.1990. London: Springer, pp. 196-200. http://link.springer.com/chapter/10.1007/978-1-4471-3810-5_16#; https://doi.org/10.1007/978-1-4471-3810-5_16

Abstract
The purpose of this extended abstract is to report on a preliminary investigation into the use of term rewriting theorem proving to support verification of formal description techniques for concurrent systems. The RRL [1, 2] system, particularly.Knuth-Bendix completion and equational proofs, is used to investigate verification of specifications written in the formal description language LOTOS. This work was completed as part of the SERC/IED ERIL project, which is investigating the use of Equational Reasoning for LOTOS. A more complete presentation of the results given here may be found in [3]. That paper also reports on complementary work, also undertaken as part of the ERIL project, using the LP theorem prover [4] for equational and inductive proofs about CSP [5].