{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:41Z","timestamp":1725663521781},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540550921"},{"type":"electronic","value":"9783540466925"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55092-5_21","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:27:51Z","timestamp":1330194471000},"page":"375-392","source":"Crossref","is-referenced-by-count":0,"title":["A mechanized theory for the verification of real-time program code using higher order logic"],"prefix":"10.1007","author":[{"given":"Rachel","family":"Cardell-Oliver","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.","DOI":"10.2307\/2266170"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013296. Springer Verlag, April 1991.","DOI":"10.1007\/3540539816_72"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013282. Springer Verlag, April 1991.","DOI":"10.1007\/3540539816_71"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-09724-4"},{"key":"21_CR5","unstructured":"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."},{"key":"21_CR6","first-page":"00","volume-title":"Fourth Refinement Workshop","author":"M. Gordon","year":"1991","unstructured":"Mike Gordon. Hard real time. In Fourth Refinement Workshop, pages 00\u201300. BCS FACS and Logica Cambridge, January 1991."},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Volkmar H. Haase. Real-time behaviour of programs. IEEE Transactions on Software Engineering, pages 494\u2013501, September 1981.","DOI":"10.1109\/TSE.1981.231111"},{"key":"21_CR8","unstructured":"Roger Hale. Safe\/0. Draft Document, May 1990."},{"key":"21_CR9","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0020-0190(89)90175-0","volume":"30","author":"E. C. R. Hehner","year":"1989","unstructured":"Eric C R Hehner. Real-time programming. Information Processing Letters, 30:51\u201356, 16 January 1989.","journal-title":"Information Processing Letters"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Jozef Hooman. A compositional proof theory for real-time distributed message passing. In PARLE: Parallel Architectures and Languages Europe. Volume II, pages 315\u2013332, June 1987. Springer Verlag Lecture Notes in Computer Science 259.","DOI":"10.1007\/3-540-17945-3_18"},{"key":"21_CR11","unstructured":"Ministry of Defence. Interim Defence Standard 00\u201355. The Procurement of Safety Critical Software in Defence Equipment. 5 April 1991"},{"key":"21_CR12","unstructured":"Johnathan S. Ostroff. Temporal Logic for Real-Time Systems. Research Studies Press, 1989."},{"issue":"7","key":"21_CR13","doi-asserted-by":"crossref","first-page":"875","DOI":"10.1109\/32.29487","volume":"15","author":"A. C. Shaw","year":"1989","unstructured":"Alan C. Shaw. Reasoning about time in higher-level language software. IEEE Transactions on Software Engineering, 15(7):875\u2013889, Jul 1989.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55092-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:57:27Z","timestamp":1605628647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55092-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540550921","9783540466925"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-55092-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}