{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:21:10Z","timestamp":1725895270759},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642104510"},{"type":"electronic","value":"9783642104527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10452-7_13","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T03:37:26Z","timestamp":1257305846000},"page":"186-203","source":"Crossref","is-referenced-by-count":2,"title":["Mechanising Data-Types for Kernel Design in Z"],"prefix":"10.1007","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system:\u00a0An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"issue":"2","key":"13_CR2","first-page":"143","volume":"18","author":"J. Bicarregui","year":"2006","unstructured":"Bicarregui, J., Hoare, T., Woodcock, J.: The verified software repository: a step towards the verifying compiler. FACJ\u00a018(2), 143\u2013151 (2006)","journal-title":"FACJ"},{"key":"13_CR3","unstructured":"Cavalcanti, A.: A Refinement Calculus for Z. PhD thesis, Oxford (1997)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11813040_6","volume-title":"FM 2006: Formal Methods","author":"E. Cohen","year":"2006","unstructured":"Cohen, E.: Validating the Microsoft Hypervisor. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, p. 81. Springer, Heidelberg (2006)"},{"key":"13_CR5","volume-title":"Formal Refinement of OS Kernels","author":"I. Craig","year":"2007","unstructured":"Craig, I.: Formal Refinement of OS Kernels, 1st edn. Springer, Heidelberg (2007)","edition":"1"},{"key":"13_CR6","unstructured":"FreeRTOS, http:\/\/www.freertos.org"},{"key":"13_CR7","unstructured":"Freitas, L.: Extended Z mathematical toolkit. Technical Report CRG13, University of York (April 2008)"},{"key":"13_CR8","unstructured":"Freitas, L.: Formal model of a reusable Chain data type. Technical Report CRG14, University of York (April 2008)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Freitas, L.: Mechanising data-types for Kernel design in Z. Technical Report CRG15, University of York (March 2009)","DOI":"10.1007\/978-3-642-10452-7_13"},{"key":"13_CR10","unstructured":"Freitas, L., Woodcock, J.: A Chain Datatype in Z. International Journal of Software Informatics (2009) (in press)"},{"key":"13_CR11","first-page":"153","volume-title":"IEEE Proceedings of 13th ICECCS, Belfast","author":"L. Freitas","year":"2008","unstructured":"Freitas, L., Woodcock, J., Buterfield, A.: POSIX and the Verification Grand Challenge:\u00a0a Roadmap. In: IEEE Proceedings of 13th ICECCS, Belfast, pp. 153\u2013162. IEEE, Los Alamitos (2008)"},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler:\u00a0A grand challenge for computing research. Journal of the ACM\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the ACM"},{"key":"13_CR13","unstructured":"ISO\/IEC 13568. Information Technology\u2014Z Formal Specification Notation\u2014Syntax, Type System and Semantics. ISO\/IEC, 1st edn. (2002)"},{"key":"13_CR14","unstructured":"ITSEC. Information technology security evaluation criteria: primary harmonised criteria. Technical Report COM(90) 314, Commission of the European Communities, version 1.2 (June 1991)"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1109\/ICECCS.2007.46","volume-title":"12th International Conference on Engineering of Complex Computer Systems (ICECCS)","author":"C. Jones","year":"2007","unstructured":"Jones, C., Pierce, K.: What can the \u03c0-calculus tell us about the mondex purse system. In: 12th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 300\u2013306. IEEE, New Zealand (2007)"},{"key":"13_CR16","volume-title":"Formal Aspects of Computing \u2014 special issue on Mondex","author":"C. Jones","year":"2008","unstructured":"Jones, C., Woodcock, J.: Formal Aspects of Computing \u2014 special issue on Mondex, vol.\u00a020(1). Springer, Heidelberg (2008)"},{"key":"13_CR17","unstructured":"Neil, M., et al.: Hypervisor Top Level Functional Specification v0.83. Technical report, Microsoft Coorporation (December 2007)"},{"key":"13_CR18","unstructured":"Saaltink, M.: Z\/Eves 2.0 Math. Toolkit. ORA, TR-99-5493-05b (October 1999)"},{"key":"13_CR19","unstructured":"Saaltink, M.: Z\/Eves 2.0 User\u2019s Guide. ORA Canada, TR-99-5493-06a (1999)"},{"key":"13_CR20","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1998","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall, Englewood Cliffs (1998)"},{"key":"13_CR21","unstructured":"Stepney, S., et al.: An Electronic Purse:\u00a0Specification, Refinement, and Proof. PRG 126, Oxford University (July 2000)"},{"key":"13_CR22","unstructured":"Stepney, S., et al.: A z patterns catalogue\u00a0vol 1. Technical Report YCS-349, University of York (2003)"},{"issue":"10","key":"13_CR23","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. IEEE Computer\u00a039(10), 57\u201364 (2006)","journal-title":"IEEE Computer"},{"key":"13_CR24","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Englewood Cliffs (1996)"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Woodcock, J., et al.: Formal methods:\u00a0practice and experience. ACM Computing Surveys (in press, 2009)","DOI":"10.1145\/1592434.1592436"},{"key":"13_CR26","unstructured":"Woodcock, J., Freitas, L., Craig, I.: A Verified Simple Operating System Kernel. In: Workshop on the Verified Software Repository as part of FM Symposium, Turku, Finland (2008), Formal Methods Europe"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10452-7_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:56:05Z","timestamp":1606168565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}