{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:16:40Z","timestamp":1740097000272,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548611"},{"type":"electronic","value":"9783642548628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_53","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:33:34Z","timestamp":1395394414000},"page":"605-619","source":"Crossref","is-referenced-by-count":0,"title":["On the Correctness of a Branch Displacement Algorithm"],"prefix":"10.1007","author":[{"given":"Jaap","family":"Boender","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"53_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A. Asperti","year":"2007","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Automated Reasoning\u00a039, 109\u2013139 (2007)","journal-title":"Automated Reasoning"},{"key":"53_CR2","unstructured":"Dickson, N.G.: A simple, linear-time algorithm for x86 jump encoding. CoRR abs\/0812.4973 (2008)"},{"key":"53_CR3","unstructured":"Hyde, R.: Branch displacement optimisation (2006), \n                    \n                      http:\/\/groups.google.com\/group\/alt.lang.asm\/msg\/d31192d442accad3"},{"key":"53_CR4","unstructured":"Intel: Intel 64 and IA-32 Architectures Developer\u2019s Manual, \n                    \n                      http:\/\/www.intel.com\/content\/www\/us\/en\/processors\/architectures-software-developer-manuals.html"},{"key":"53_CR5","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043, 363\u2013446 (2009), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/s10817-009-9155-4\n                    \n                    \n                  , doi: 10.1007\/s10817-009-9155-4","journal-title":"Journal of Automated Reasoning"},{"key":"53_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-35308-6_7","volume-title":"Certified Programs and Proofs","author":"D.P. Mulligan","year":"2012","unstructured":"Mulligan, D.P., Sacerdoti Coen, C.: On the correctness of an optimising assembler for the intel MCS-51 microprocessor. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 43\u201359. Springer, Heidelberg (2012), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/978-3-642-35308-6_7"},{"issue":"1","key":"53_CR7","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1145\/357062.357067","volume":"1","author":"E.L. Robertson","year":"1979","unstructured":"Robertson, E.L.: Code generation and storage allocation for machines with span-dependent instructions. ACM Trans. Program. Lang. Syst.\u00a01(1), 71\u201383 (1979), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/357062.357067","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"53_CR8","unstructured":"Small device C compiler 3.1.0 (2011), \n                    \n                      http:\/\/sdcc.sourceforge.net\/"},{"issue":"4","key":"53_CR9","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1145\/359460.359474","volume":"21","author":"T.G. Szymanski","year":"1978","unstructured":"Szymanski, T.G.: Assembling code for machines with span-dependent instructions. Commun. ACM\u00a021(4), 300\u2013308 (1978), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/359460.359474","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_53","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T08:15:02Z","timestamp":1558858502000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}