Publications related to Logic, Term Rewriting and Algebraic Semantics

1. D. Graham, M. Calder, and A Miller
An Inductive Technique for Parameterised Model Checking of Degenerative Distributed Randomised Protocols
Proceedings of AVOCS 07 (Automated Verification of Critical Systems), ENTCS vol. 250, pp.87-103, Elsevier 2009.

2. A. Miller, A. Donaldson and M. Calder
Symmetry in temporal logic model checking
Computing Surveys, ACM ,vol. 38, issue 3,pp. 1-36, 2006.

3. A. Miller, M. Calder and A. Donaldson
A template-based approach for the generation of abstractable and reducible models of featured networks
Computer Networks, vol. 51(2), pp. 439-455, Elsevier, 2007.

4. M Calder and A. Miller.
Verifying parameterised, featured networks by abstraction
Proceedings of the first International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), pp 227--234.

5. M. Calder and A. Miller.
Five ways to use symmetry and induction in the verification of networks of processes using model-checking.
Proceedings of Automated Verification of Critical Systems (AVoCS),2002.

6. M. Calder, S. Maharaj, and C. Shankland.
A Modal Logic for Full LOTOS based on Symbolic Transition Systems.
The Computer Journal, Volume 45, No.1, pp. 55--61, 2002.

7. M. Calder, S. Maharaj, and C. Shankland.
An Adequate Logic for Full LOTOS.
Proceedings of FME 2001, Lecture Notes in Computer Science. vol. 2021, pp.384-395, 2001.

8. M. Calder and C. Shankland.
A Symbolic Semantics and Bisimulation for Full LOTOS.
Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems, Korea, 2001. M.Kim, B.Chin, S.Kang and D.Lee (Eds.), pp. 184--200, Kluwer Academic Publishers, 2001.

9. M. Thomas and P. Watson.
Solving Divergence in Knuth-Bendix Completion by Enriching Signatures.
Theoretical Computer Science (Elsevier) 112 pp. 145 - 185, 1993.

10. M. Thomas.
Algebraic Semantics. Chapter 4
in D.A. Watt, Programming Language Syntax and Semantics pp. 147-183, Prentice Hall 1991.

11. M. Thomas and P. Watson.
Generalising Sequences of Rewrite Rules by Synthesising New Sorts.
Extended Abstract, Functional Programming, Glasgow 1990, pp.268-273, Workshops in Computing, S. Peyton-Jones, G. Hutton, C. Kehler Holst (eds.), Springer-Verlag 1991.

12. M. Thomas and K. Jantke
Inductive Inference for Knuth Bendix Completion
Lecture Notes in Computer Science vol. 397 288-303, Springer Verlag, 1989.

13. M. Thomas
Implementing Algebraically Specified Abstract Data Types in an Imperative Programming Language
Proceedings of TAPSOFT 87, Lecture Notes in Computer Science vol. 250 197-211, Springer Verlag, 1987.