H.R. Andersen. Model checking and boolean graphs. In B. Krieg-Brückner, editor, Proceedings of the 4th European Symposium on Programming (ESOP'92), volume 582 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
 H.R. Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Århus Universitet, 1993.
 W. Atkinson and J. Cunningham. Proving properties of a safety critical system. Software Engineering Journal, 6(2):41--50, 1991.
 A. Beveniste. Synchronous languages provide safety in reactive system design. Control Engineering, Sept. 1994.
 G.M. Birtwistle and P.A. Subrahmanyam, editors. Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989. Proceedings of the 1988 Banff Workshop on Hardware Verification.
 T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, North-Holland, 14:25--59, 1987.
 A railway signalling case study for FOREST. Internal publication by British Rail Research, London Rd., Derby, England, 1988. Issue B, ELS-DOC-4314.
 SSI Data Preparation Guide. Published by British Railways Board, Feb. 1990. ELS-DOC-3080, Issue K of SSI8003-INT and supplements; British Rail Research, London Road, Derby, England.
 J. Bradfield and C. Stirling. Local model checking for infinite state spaces. Theoretical Computer Science, 96:157--174, 1992.
 J.C. Bradfield. Verifying Temporal Properties of Systems with Applications to Petri Nets. PhD thesis, University of Edinburgh, 1991. Available as CST-83-91.
 R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--91, 1986.
 J.R. Burch, E.M. Clark, et al. Symbolic model checking: 10^20 states and beyond. In Proceedings of Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428--39. Computer Society Press, 1990.
 J.R. Burch, E.M. Clark, et al. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 13(4):401--24, 1994.
 J. Camilleri and T. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, 1993.
 K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
 A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(1):56--68, 1940.
 E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244--63, 1986.
 R. Cleaveland. Tableau-based model checking in the modal mu-calculus. Acta Informatica, 27:725--47, 1990.
 R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics-based verification tool for finite-state systems. In Proceedings of the 9th IFIP Symposium on Protocol Specification, Testing and Verification, pages 287--302. North-Holland, 1989.
 G.V. Conroy and C. Pulley. Logical methods in the formal verification of safety-critical software. Presented at the IMA Conference on Dependable Computing, Sept. 1993.
 D. Craigen, S. Gerhart, and T. Ralston. An International Survey of Industrial Applications of Formal Methods---Purpose, Approach, Analysis and Conclusions, volume 1. NIST (National Institute of Standards and Technology), 1993.
 D. Craigen, S. Gerhart, and T. Ralston. An International Survey of Industrial Applications of Formal Methods---Case Studies, volume 2. NIST (National Institute of Standards and Technology), 1993.
 A.H. Cribbens. Solid State Interlocking (SSI): an integrated electronic signalling system for mainline railways. Proc. IEE, 134(3):148--58, 1987.
 A.H. Cribbens and I.H. Mitchell. The application of advanced computer techniques to the generation and checking of SSI data. Proceedings of the Institute of Railway Signalling Engineers, 1992.
 W.J. Cullyer and W. Wong. Application of formal methods to railway signalling---a case study. IEE Computing and Control Engineering Journal, 4(1):15--22, 1993.
 R. de Simone. Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science, 37:245--67, 1985.
 E.A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science , chapter 16.
 E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the modal mu-calculus. In Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science, pages 267--78. Computer Sociecty Press, 1986.
 R. Enders, T. Filkorn, and D. Tauber. Generating BDDs for symbolic model checking in CCS. In Proceedings of the 3rd Workshop on Computer Aided Verification, 1991.
 A. Fantechi, S. Gnesi, and G. Ristori. Model checking for action-based logics. Formal Methods in System Design, 4:187--203, 1994.
 S. Fisched, A. Scholz, and D. Taubner. Verification in process algebra of the distributed control of track vehicles---a case study. Formal Methods in System Design, 4(2):99--122, 1994.
 R. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science. American Mathematical Society, 1967.
 M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In G.M. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer International Series in Engineering and Computer Science, pages 73--128. Kluwer, Boston, 1988.
 M.J.C. Gordon. Mechanizing programming logics in higher-order logic. In Birtwistle and Subrahmanyam , pages 387--439.
 M.J.C. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
 J. Groote, J. Koorn, and S. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd (extended abstract). In Proceedings of the 10th Annual Conference on Computer Assurance (COMPASS'95), pages 57--68, Gaithersburg, Maryland, 1995.
 A. Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, 1:151--238, 1992.
 W.A. Halang and B.J. Krämer. Safety assurance in process control. IEEE Software, pages 61--7, Jan. 1994.
 J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38(5), 1995.
 M. Hennessey. Algebraic Theory of Processes. Foundations of Computing. MIT Press, London, 1988.
 M. Hennessy and R. Milner. On observing nondeterminism and concurrency. In Proceedings of the 7th Colloquium on Automata, Languages and Programming, volume 85 of Lecture Notes in Computer Science, pages 299--309. Springer-Verlag, 1980.
 M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137--161, 1985.
 C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10), 1969.
 C.A.R. Hoare. Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, 1985.
 Software for computers in the application of industrial safety-related systems. International Electrotechnical Commission, 1994. IEC Standard 1131, Part 3.
 M. Ingleby. A Galois theory of local reasoning in control systems with compositionality. Presented at the IMA Conference on Dependable Computing, Sept. 1993.
 M. Ingleby and I. Mitchell. Proving safety of a railway signalling system incorporating geographic data. In Proceedings of SAFECOMP'92, pages 129--134. IFAC, Pergamon Press, 1992.
 A. Jowett. Jowett's Railway Atlas of Great Britain and Ireland. Patrick Stephens Ltd. (Haynes), 1989. ISBN: 1-85260-086-1.
 J. Joyce and C. Seger, editors. Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
 T. King. Formalising British Rail's signalling rules. In Proceedings FME'94: Industrial Benefit of Formal Methods, volume 873 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
 D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333--54, 1983.
 L. Lamport. The temporal logic of actions. Technical Report 79, Digital Systems Research Center, 1991.
 K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72:265--88, 1990.
 S. Malik. Analysis of cyclic combinational circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 13(7), 1994.
 K. Mark Hansen. Formalising railway interlocking systems. Technical report, Department of Computer Science, Technical University of Denmark, July 1994. Presented at the Nordic Seminar on Dependable Computing Systems.
 K.L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon, 1992.
 T.F. Melham. Automating recursive type definitions in higher order logic. In Birtwistle and Subrahmanyam , pages 341--86. Proceedings of the 1988 Banff Workshop on Hardware Verification.
 R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267--310, 1983.
 R. Milner. The use of machines to assist in rigorous proof. Phil. Trans. R. Soc. Lond., 312:411--22, 1984.
 R. Milner. A Calculus of Communicating Systems. Springer-Verlag, 1990.
 R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1990.
 R. Milner. Interpreting one concurrent calculus in another. Theoretical Computer Science, 75:3--13, 1990.
 R. Milner. Operational and algebraic semantics of concurrent processes. In Handbook of Theoretical Computer Science , chapter 19.
 R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209--22, 1990.
 I.H. Mitchell. Proposal for an SSI data checking tool. Internal publication by British Rail Research, London Rd., Derby. DE2 8YB, June 1990.
 I.H. Mitchell, Nov. 1995. Personal communication.
 The procurement of safety critical software in defence equipment (Guidance). UK Ministry of Defence, Apr. 1991. (Interim) Defence Standard 00-55, Part 1.
 The procurement of safety critical software in defence equipment (Requirements). UK Ministry of Defence, Apr. 1991. (Interim) Defence Standard 00-55, Part 2.
 Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment. UK Ministry of Defence, Apr. 1991. (Interim) Defence Standard 00-56.
 F. Moller and C. Tofts. A temporal calculus of communicating systems. In Proceedings of CONCUR'90, volume 458 of Lecture Notes in Computer Science, pages 401--15, 1990.
 M.J. Morley. An heuristic approach to state space reduction of communicating parallel systems. Master's thesis, University of Edinburgh, 1989. Summarised in .
 M.J. Morley. Tactics for state space reduction on the CWB. Technical Report ECS-LFCS-90-109, Laboratory for Foundations of Computer Science, University of Edinburgh, 1990.
 M.J. Morley. Modelling British Rail's interlocking logic: Geographic data correctness. Technical Report ECS-LFCS-91-186, Laboratory for Foundations of Computer Science, University of Edinburgh, 1991.
 M.J. Morley. Safety in railway signalling data: A behavioural analysis. In Joyce and Seger , pages 465--74.
 O.S. Nock. Railway Signalling---a treatise on the recent practice of British Railways. Adam and Charles Black, London, 1980. Prepared under the direction of a committee of the Institution of Railway Signalling Engineers under the general direction of O. S. Nock.
 S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748--52. Springer-Verlag, 1992.
 D. Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, 1981.
 L.C. Paulson. The Isabelle Reference Manual. Computer Laboratory, University of Cambridge, 1993.
 A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In Current trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510--84. Springer-Verlag, 1986.
 V. Pratt. A decidable mu-calculus. In Proceedings of the 22nd Annual IEEE Symposium on Foundations of Computer Science, pages 421--427, 1981.
 G.M. Reed and A. Roscoe. A timed model of communication sequential processes. In Proceedings of ICALP'86, volume 226 of Lecture Notes in Computer Science, pages 314--23. Springer-Verlag, 1986.
 J. Rushby. Formal methods in the certification of critical systems. Technical Report CSL-93-7, SRI International, 1993. Also: NASA CR 4551 Formal Methods and Digital Systems Validation for Airborne Systems.
 B. Sanders. Eliminating the Substitution Axiom from UNITY logic. Formal Aspects of Computing, 3(2):189--285, 1991.
 R.C. Short. Software validation for a railway signalling system. In Proceedings of SAFECOMP'83, pages 183--193. IFAC, Pergamon Press, 1983.
 K. Slind. AC unification in hol90. In Joyce and Seger , pages 437--49.
 G. Stålmarck. A proof theoretic concept of tautological hardness. Incomplete manuscript circulated to interested parties for review., May 1994.
 G. Stålmarck and M. Säflund. Modelling and verifying systems and software in propositional logic. In Proceedings of SAFECOMP'90, pages 31--6. IFAC, Pergamon Press, 1990.
 C. Stirling. Modal and temporal logics for processes. Technical Report ECS-LFCS-92-221, Laboratory for Foundations of Computer Science, University of Edinburgh, 1992. Lecture notes for the 4th European Summer School in Logic, Language and Information, University of Essex.
 C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT'89), volume 351 of Lecture Notes in Computer Science, pages 368--82. Springer-Verlag, 1989.
 C. Stirling and D. Walker. A general tableau technique for verifying temporal properties of concurrent programs. In Proceedings of the International BCS-FACS Workshop on Semantics for Concurrency, Workshops in Computing, pages 1--15, Berlin, 1990. Springer-Verlag.
 D. Syme. A new interface for HOL - ideas, issues and implementation. In T.E. Schubert and P.J. Windley, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science. Springer-Verlag, 1995.
 R.D. Tennent. Semantics of Programming Languages. International Series in Computer Science. Prentice Hall International, 1991.
 L. Thèry, Y. Bertot, and G. Kahn. Real theorem provers deserve real user interfaces. In Proceedings of the fifth ACM SIGSOFT Symposium on Software Development Environments, volume 17 of Software Engineering Notes, 1992.
 C. Tofts. Proof Systems and Pragmatics for Parallel Programming. PhD thesis, University of Edinburgh, 1990.
 J. van Leeuwen. Handbook ot Theoretical Computer Science, volume B. Elsevier, 1990.
 D. Walker. Automated analysis of mutual exclusion algorithms using CCS. Formal Aspects of Computing, 1:273--92, 1989.
Unpublished, although available on-line., 1993.
 W. Wong. A Formal Theory of Railway Track Networks in Higher-order Logic and its Applications in Interlocking Design. PhD thesis, University of Warwick, 1991.
Modelling bit vectors in HOL: the
In Joyce and Seger
, pages 371--84.