{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T17:40:30Z","timestamp":1687542030469},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T00:00:00Z","timestamp":1466985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T00:00:00Z","timestamp":1466985600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"SENSATION project","award":["318490"],"award-info":[{"award-number":["318490"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Inf Syst Front"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10796-016-9665-7","type":"journal-article","created":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T05:35:07Z","timestamp":1467005707000},"page":"909-925","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal modelling and analysis of Bitflips in ARM assembly code"],"prefix":"10.1007","volume":"18","author":[{"given":"Ren\u00e9 Rydhof","family":"Hansen","sequence":"first","affiliation":[]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Mads Chr.","family":"Olesen","sequence":"additional","affiliation":[]},{"given":"Erik Ramsgaard","family":"Wognsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,27]]},"reference":[{"key":"9665_CR1","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A.C.J., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., & Nardelli, F.Z. (2009). The semantics of POWER and ARM multiprocessor machine code. In Proceedings of workshop on declarative aspects of multicore programming (DAMP) (pp. 13\u201324). ACM.","DOI":"10.1145\/1481839.1481842"},{"key":"9665_CR2","unstructured":"ARM Ltd. (2005). ARM Architecture Reference Manual. Issue I."},{"key":"9665_CR3","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., & Reps, T.W. (2004). Analyzing memory accesses in x86 executables. In Proceedings of compiler construction (CC), lecture notes in computer science, (Vol. 2985, pp. 5\u201323). Springer.","DOI":"10.1007\/978-3-540-24723-4_2"},{"issue":"6","key":"9665_CR4","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MM.2005.110","volume":"25","author":"S Borkar","year":"2005","unstructured":"Borkar, S. (2005). Designing reliable systems from unreliable components: the challenges of transistor variability and degradation. IEEE Micro, 25(6), 10\u201316.","journal-title":"IEEE Micro"},{"key":"9665_CR5","doi-asserted-by":"crossref","unstructured":"Brumley, D., Jager, I., Avgerinos, T., & Schwartz, E.J. (2011). BAP: A binary analysis platform. In Proceedings of computer aided verification (CAV), lecture notes in computer science, (Vol. 6806, pp. 463\u2013469). Springer.","DOI":"10.1007\/978-3-642-22110-1_37"},{"key":"9665_CR6","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., & Wang, Z. (2011). Time for statistical model checking of real-time systems. In Proceedings of computer aided verification (CAV), lecture notes in computer science, (Vol. 6806, pp. 349\u2013355). Springer.","DOI":"10.1007\/978-3-642-22110-1_27"},{"issue":"5","key":"9665_CR7","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1145\/502102.502104","volume":"48","author":"AY Halevy","year":"2001","unstructured":"Halevy, A.Y., Mumick, I.S., Sagiv, Y., & Shmueli, O. (2001). Static analysis in datalog extensions. Journal of the ACM, 48(5), 971\u20131012.","journal-title":"Journal of the ACM"},{"key":"9665_CR8","doi-asserted-by":"publisher","unstructured":"Hansen, R.R., Larsen, K.G., Olesen, M.C., & Wognsen, E.R. (2015). Formal methods for modelling and analysis of single-event upsets. In Proceedings of the 3rd IEEE international workshop on formal methods integration (FMi 2015), (pp. 287\u2013294). IEEE. doi:10.1109\/IRI.2015.54. Published as part of the proceedings of the IEEE International Conference on Information Reuse and Integration (IRI 2015).","DOI":"10.1109\/IRI.2015.54"},{"key":"9665_CR9","unstructured":"Heintze, N., & Jaffar, J. (1990). A decision procedure for a class of set constraints (extended abstract). In Proceedings of logic in computer science (LICS), (pp. 42\u201351)."},{"issue":"1","key":"9665_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., & Yi, W. (1997). UPPAAL In a nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1(1), 134\u2013152.","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"9665_CR11","doi-asserted-by":"crossref","unstructured":"Meola, M.L., & Walker, D. (2010). Faulty logic: reasoning about fault tolerant programs. In Proceedings of programming languages and systems (ESOP), (pp. 468\u2013487). Springer.","DOI":"10.1007\/978-3-642-11957-6_25"},{"key":"9665_CR12","doi-asserted-by":"crossref","unstructured":"Nicolescu, B., & Velazco, R. (2003). Detecting soft errors by a purely software approach: method, tools and experimental results. In Proceedings of design, automation & test in Europe (DATE), (pp. 20,057\u201320,063).","DOI":"10.1109\/DATE.2003.1253806"},{"key":"9665_CR13","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., & Hankin, C. (1999). Principles of program analysis: Springer.","DOI":"10.1007\/978-3-662-03811-6"},{"issue":"9","key":"9665_CR14","first-page":"335","volume":"2002","author":"F Nielson","year":"2002","unstructured":"Nielson, F., Nielson, H.R., & Seidl, H. (2002). A succinct solver for ALFP. Nordic Journal of Computing, 2002(9), 335\u2013372.","journal-title":"Nordic Journal of Computing"},{"issue":"6","key":"9665_CR15","doi-asserted-by":"publisher","first-page":"2742","DOI":"10.1109\/23.556861","volume":"43","author":"E Normand","year":"1996","unstructured":"Normand, E. (1996). Single event upset at ground level. IEEE Transactions on Nuclear Science, 43(6), 2742\u20132750.","journal-title":"IEEE Transactions on Nuclear Science"},{"issue":"1","key":"9665_CR16","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1109\/24.994926","volume":"51","author":"N Oh","year":"2002","unstructured":"Oh, N., Shirvani, P.P., & McCluskey, E.J. (2002). Control-flow checking by software signatures. IEEE Transactions on Reliability, 51(1), 111\u2013122.","journal-title":"IEEE Transactions on Reliability"},{"issue":"1","key":"9665_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1109\/24.994913","volume":"51","author":"N Oh","year":"2002","unstructured":"Oh, N., Shirvani, P.P., & McCluskey, E.J. (2002). Error detection by duplicated instructions in super-scalar processors. IEEE Transactions on Reliability, 51(1), 63\u201375.","journal-title":"IEEE Transactions on Reliability"},{"key":"9665_CR18","doi-asserted-by":"crossref","unstructured":"Pattabiraman, K., Nakka, N., Kalbarczyk, Z., & Iyer, R.K. (2008). SymPLFIED: Symbolic program-level fault injection and error detection framework. In Proceedings of dependable systems and networks (DSN), (pp. 472\u2013481).","DOI":"10.1109\/DSN.2008.4630118"},{"key":"9665_CR19","doi-asserted-by":"crossref","unstructured":"Perry, F., Mackey, L.W., Reis, G.A., Ligatti, J., August, D.I., & Walker, D. (2007). Fault-tolerant typed assembly language. In Proceedings of programming language design and implementation (PLDI), (pp. 42\u201353). ACM.","DOI":"10.1145\/1273442.1250741"},{"key":"9665_CR20","doi-asserted-by":"crossref","unstructured":"Perry, F., & Walker, D. (2008). Reasoning about control flow in the presence of transient faults. In Proceedings of static analysis symposium (SAS), lecture notes in computer science, (Vol. 5079, pp. 332\u2013346). Springer.","DOI":"10.1007\/978-3-540-69166-2_22"},{"key":"9665_CR21","doi-asserted-by":"crossref","unstructured":"Reis, G.A., Chang, J., Vachharajani, N., Rangan, R., & August, D.I. (2005). SWIFT: software implemented fault tolerance. In Proceedings of symposium on code generation and optimization (CGO), (pp. 243\u2013254).","DOI":"10.1109\/CGO.2005.34"},{"issue":"6","key":"9665_CR22","doi-asserted-by":"publisher","first-page":"1822","DOI":"10.1109\/23.983136","volume":"48","author":"GM Swift","year":"2001","unstructured":"Swift, G.M., Fannanesh, F.F., Guertin, S.M., Irom, F., & Millward, D.G. (2001). Single-event upset in the powerPC750 microprocessor. IEEE Transactions on Nuclear Science, 48(6), 1822\u20131827.","journal-title":"IEEE Transactions on Nuclear Science"},{"key":"9665_CR23","doi-asserted-by":"crossref","unstructured":"Underwood, C.I., Ecoffet, R., Duzeffier, S., & Faguere, D. (1993). Observations of single-event upset and multiple-bit upset in non-hardened high-density SRAMs in the TOPEX\/poseidon orbit. In Radiation effects data IEEE workshop, (pp. 85\u201392).","DOI":"10.1109\/REDW.1993.700572"},{"key":"9665_CR24","doi-asserted-by":"crossref","unstructured":"Wang, F., & Agrawal, V.D. (2008). Single event upset: an embedded tutorial. In Proceedings of VLSI design (VLSID), (p. 429).","DOI":"10.1109\/VLSI.2008.28"},{"key":"9665_CR25","doi-asserted-by":"crossref","unstructured":"Wang, N.J., Quek, J., Rafacz, T.M., & Patel, S.J. (2004). Characterizing the effects of transient faults on a High-Performance processor pipeline. In Proceedings of dependable systems and networks (DSN), (pp. 61\u201371).","DOI":"10.1109\/DSN.2004.1311877"},{"key":"9665_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, M., Liu, Z., Morisset, C., & Ravn, A.P. (2009). Design and verification of fault-tolerant components. In Methods, models and tools for fault tolerance, lecture notes in computer science, (Vol. 5454, pp. 57\u201384). Springer.","DOI":"10.1007\/978-3-642-00867-2_4"}],"container-title":["Information Systems Frontiers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10796-016-9665-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-016-9665-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-016-9665-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10796-016-9665-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T17:00:06Z","timestamp":1687539606000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10796-016-9665-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,27]]},"references-count":26,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["9665"],"URL":"https:\/\/doi.org\/10.1007\/s10796-016-9665-7","relation":{},"ISSN":["1387-3326","1572-9419"],"issn-type":[{"value":"1387-3326","type":"print"},{"value":"1572-9419","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,27]]},"assertion":[{"value":"27 June 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}