{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:44:29Z","timestamp":1725518669634},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540876021"},{"type":"electronic","value":"9783540876038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87603-8_21","type":"book-chapter","created":{"date-parts":[[2008,9,20]],"date-time":"2008-09-20T07:56:24Z","timestamp":1221897384000},"page":"265-279","source":"Crossref","is-referenced-by-count":1,"title":["Using EventB to Create a Virtual Machine Instruction Set Architecture"],"prefix":"10.1007","author":[{"given":"Stephen","family":"Wright","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"AMD Inc. 28-Bit SSE5 Instruction Set (2007)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Audsely, N.: Portable Code in Future Avionic Systems, IEE Colloquium on Real-Time Systems (Digest No. 1998\/306) (1998)","DOI":"10.1049\/ic:19980524"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S.: RuleBase: Model checking at IBM. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"21_CR4","unstructured":"Butler, M.: RODIN Deliverable D16 Prototype Plug-in Tools (2006), http:\/\/rodin.cs.ncl.ac.uk"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Caset, L.: Formal Development of an Embedded Verifier for Java Card Byte Code. In: International Conference on Dependable Systems and Networks (2002)","DOI":"10.1109\/DSN.2002.1028886"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Evans, N., Butler, M.: A Proposal for Records in Event-B Formal Methods 2006 (2006)","DOI":"10.1007\/11813040_16"},{"key":"21_CR7","volume-title":"Computer Architecture, A Quantitive Approach","author":"J. Hennessy","year":"2003","unstructured":"Hennessy, J., Patterson, D.: Computer Architecture, A Quantitive Approach. Morgan Kaufmann, San Francisco (2003)"},{"key":"21_CR8","unstructured":"Hitachi Ltd. SH7707 Hardware Manual (1998)"},{"key":"21_CR9","volume-title":"The C Programming Language","author":"B. Kernighan","year":"1988","unstructured":"Kernighan, B., Ritchie, D.: The C Programming Language. Prentice Hall, Englewood Cliffs (1988)"},{"key":"21_CR10","doi-asserted-by":"crossref","DOI":"10.1109\/9780470544433","volume-title":"DSP Processor Fundamentals","author":"P. Lapsley","year":"1997","unstructured":"Lapsley, P., Bier, J., Shoham, A., Lee, E.: DSP Processor Fundamentals. IEEE Press, Los Alamitos (1997)"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Lee, E.: Programmable DSP Processors part I and II. IEEE ASSP Mag. (October 1988\u2013January 1989)","DOI":"10.1109\/53.16934"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: FME 2003, SpringerLink (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"21_CR13","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn (1999)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Lowry, H., Mitchell, B.: Mission computer replacement prototype for Special Operations Forces aircraft an application of commercial technology to avionics. In: Proceedings of The 19th Digital Avionics Systems Conference (2000)","DOI":"10.1109\/DASC.2000.886960"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Luke, J., Haldeman, D.: Replacement Strategy for Aging Avionics Computers. IEEE Aerospace and Electronic Systems Magazine\u00a014(3) (1999)","DOI":"10.1109\/62.750422"},{"key":"21_CR16","unstructured":"Metayer, C., Abrial, J.-R., Voisin, L.: RODIN Deliverable 3.2 Event-B Language (2005), http:\/\/rodin.cs.ncl.ac.uk"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Moore, J.: A Grand Challenge Proposal for Formal Methods A Verified Stack. In: Formal Methods at the Crossroads From Panacea to Foundational Support, SpringerLink (2003)","DOI":"10.1007\/978-3-540-40007-3_11"},{"key":"21_CR18","unstructured":"Schneider, S.: The B-Method An Introduction. Palgrave (2001)"},{"key":"21_CR19","volume-title":"The Java Developer\u2019s Guide to Eclipse","author":"S. Shavor","year":"2003","unstructured":"Shavor, S., D\u2019Anjou, J., Fairbrother, S.: The Java Developer\u2019s Guide to Eclipse. Addison-Wesley, Reading (2003)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Sherridan, F.: Practical Testing of a C99 Compiler Using Output Comparison. Software: Practical and Experience\u00a037(14) (2007)","DOI":"10.1002\/spe.812"},{"key":"21_CR21","unstructured":"Stallman, R.: Using and Porting the GNU Compiler Collection, Free Software Foundation (2001)"},{"key":"21_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R. Stark","year":"2001","unstructured":"Stark, R., Schmid, J., Borger, E.: Java and the Java Virtual Machine. Springer, Heidelberg (2001)"},{"key":"21_CR23","volume-title":"Practical Model-Based Testing \u2013 A Tools Approach","author":"M. Utting","year":"2007","unstructured":"Utting, M., Legeard, B.: Practical Model-Based Testing \u2013 A Tools Approach. Morgan Kaufmann, San Francisco (2007)"},{"key":"21_CR24","unstructured":"Voisin, L.: A Description of the RODIN Prototype (2006), http:\/\/rodin.cs.ncl.ac.uk"},{"key":"21_CR25","unstructured":"Wright, S.: MIDAS Design Document CSTR-06-014, Bristol University (2008), http:\/\/www.cs.bris.ac.uk\/Publications\/Papers\/2000543.pdf"},{"key":"21_CR26","unstructured":"http:\/\/www.hercules-390.org\/"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, B and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87603-8_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:05:09Z","timestamp":1606183509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87603-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540876021","9783540876038"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87603-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}