{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T02:40:19Z","timestamp":1739414419997,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642104510"},{"type":"electronic","value":"9783642104527"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10452-7_19","type":"book-chapter","created":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T08:37:26Z","timestamp":1257323846000},"page":"282-289","source":"Crossref","is-referenced-by-count":1,"title":["Formal Modelling of a Microcontroller Instruction Set in B"],"prefix":"10.1007","author":[{"suffix":"Jr.","given":"Val\u00e9rio","family":"Medeiros","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book: Assigning Programs to Meanings, 1st edn. Cambridge University Press, USA (1996)","edition":"1"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Aljer, P.D., Boulanger, S.T.J.-L., Bhdl, G.M.: Circuit Design in B. A. In: ACSD, Third International Conference on Application of Concurrency to System Design, pp. 241\u2013242 (2003)","DOI":"10.1109\/CSD.2003.1207723"},{"key":"19_CR3","unstructured":"Casset, L., Lanet, J.L.: A Formal Specification of the Java Bytecode Semantics using the B method. Technical Report, Gemplus (1999)"},{"key":"19_CR4","unstructured":"Dantas, B., D\u00e9harbe, D., Galv\u00e3o, S.L., Moreira, A.M., Medeiros Jr., V.G.: Applying the B Method to Take on the Grand Challenge of Verified Compilation. In: SBMF, Savaldor (2008), SBC"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-540-30579-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C.A.R. Hoare","year":"2005","unstructured":"Hoare, C.A.R.: The verifying compiler, a grand challenge for computing research. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, p. 78. Springer, Heidelberg (2005)"},{"key":"19_CR6","unstructured":"Zilog. Z80 Family CPU User Manual, http:\/\/www.zilog.com\/docs\/z80\/um0080.pdf"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10452-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T02:01:22Z","timestamp":1739412082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10452-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642104510","9783642104527"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10452-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}