A mechanized theory for the verification of real-time program code using higher order logic

1. A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.

   Google Scholar 

2. A. Camilleri, P. Iverardi, and M. Nesi. Combining interaction and automation in process algebra verification. In TAPSOFT '91, number 494 in Lecture Notes in Computer Science, pages 283–296. Springer Verlag, April 1991.

   Google Scholar 

3. Rachel Cardell-Oliver. Using higher order logic for modelling real-time protocols. In TAPSOFT '91, number 494 in Lecture Notes in Computer Science, pages 259–282. Springer Verlag, April 1991.

   Google Scholar 

4. M.J.C. Gordon, A.J.R.G. Milner, and C.P. Wadsworth. Edinburgh LCF: a mechanized logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.

   Google Scholar 

5. Michael J.C. Gordon. Mechanizing programming logics in higher order logic. Technical Report 145, Computer Laboratory, University of Cambridge, September 1988. published in 1988 Banff Conf on Hardware Verification.

   Google Scholar 

6. Mike Gordon. Hard real time. In Fourth Refinement Workshop, pages 00–00. BCS FACS and Logica Cambridge, January 1991.

   Google Scholar 

7. Volkmar H. Haase. Real-time behaviour of programs. IEEE Transactions on Software Engineering, pages 494–501, September 1981.

   Google Scholar 

8. Roger Hale. Safe/0. Draft Document, May 1990.

   Google Scholar 

9. Eric C R Hehner. Real-time programming. Information Processing Letters, 30:51–56, 16 January 1989.

   Google Scholar 

10. Jozef Hooman. A compositional proof theory for real-time distributed message passing. In PARLE: Parallel Architectures and Languages Europe. Volume II, pages 315–332, June 1987. Springer Verlag Lecture Notes in Computer Science 259.

    Google Scholar 

11. Ministry of Defence. Interim Defence Standard 00–55. The Procurement of Safety Critical Software in Defence Equipment. 5 April 1991

    Google Scholar 

12. Johnathan S. Ostroff. Temporal Logic for Real-Time Systems. Research Studies Press, 1989.

    Google Scholar 

13. Alan C. Shaw. Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering, 15(7):875–889, Jul 1989.

    Google Scholar 

Download references