{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:43:12Z","timestamp":1761324192235},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319989341"},{"type":"electronic","value":"9783319989358"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98935-8_1","type":"book-chapter","created":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T21:19:26Z","timestamp":1544131166000},"page":"1-21","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Robust Digital Computation in the Physical World"],"prefix":"10.1007","author":[{"given":"Jackson R.","family":"Mayo","sequence":"first","affiliation":[]},{"given":"Robert C.","family":"Armstrong","sequence":"additional","affiliation":[]},{"given":"Geoffrey C.","family":"Hulette","sequence":"additional","affiliation":[]},{"given":"Maher","family":"Salloum","sequence":"additional","affiliation":[]},{"given":"Andrew M.","family":"Smith","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"J.R. Abrial, Modeling in Event-B: System and Software Engineering, 1st edn. (Cambridge University Press, Cambridge, 2010)","edition":"1"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"Rajeev Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, T.A. Henzinger, P.H. Ho, Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, in Hybrid Systems, ed. by R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel. Lecture Notes in Computer Science, vol. 736 (Springer, Heidelberg, 1993), pp. 209\u2013229"},{"issue":"7","key":"1_CR3","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1109\/TC.1983.1676292","volume":"32","author":"JC Barros","year":"1983","unstructured":"J.C. Barros, B.W. Johnson, Equivalence of the arbiter, the synchronizer, the latch, and the inertial delay. IEEE Trans. Comput. 32(7), 603\u2013614 (1983)","journal-title":"IEEE Trans. Comput."},{"key":"1_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Y. Bertot, P. Cast\u00e9ran, Interactive Theorem Proving and Program Development (Springer, Heidelberg, 2004)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"S. Boldo, C. Lelay, G. Melquiond, Improving real analysis in Coq: a user-friendly approach to integrals and derivatives, in CPP\u201912, ed. by C. Hawblitzel, D. Miller. Lecture Notes in Computer Science, vol. 7679 (Springer, Heidelberg, 2012), pp. 289\u2013304","DOI":"10.1007\/978-3-642-35308-6_22"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1016\/j.jpdc.2008.12.002","volume":"69","author":"G Bosilca","year":"2009","unstructured":"G. Bosilca, R. Delmas, J. Dongarra, J. Langou, Algorithm-based fault tolerance applied to high performance computing. J. Parallel Distrib. Comput. 69, 410\u2013416 (2009)","journal-title":"J. Parallel Distrib. Comput."},{"issue":"1","key":"1_CR7","first-page":"5","volume":"1","author":"F Cappello","year":"2014","unstructured":"F. Cappello, A. Geist, W. Gropp, S. Kale, B. Kramer, M. Snir, Toward exascale resilience: 2014 update. Supercomput. Front. Innov. 1(1), 5\u201328 (2014)","journal-title":"Supercomput. Front. Innov."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: an opensource tool for symbolic model checking, in Proceedings of the 14th International Conference on Computer Aided Verification (2002), pp. 359\u2013364","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"S.A. Cook, The complexity of theorem-proving procedures, in Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (1971), pp. 151\u2013158","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"1_CR11","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/JPROC.2011.2160929","volume":"100","author":"P. Derler","year":"2012","unstructured":"P. Derler, E.A. Lee, A. Sangiovanni-Vincentelli, Modeling cyber-physical systems. Proc. IEEE (special issue on CPS) 100(1), 13\u201328 (2012)","journal-title":"Proceedings of the IEEE"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"G. Fey, Assessing system vulnerability using formal verification techniques, in Mathematical and Engineering Methods in Computer Science, ed. by Z. Kot\u00e1sek, J. Bouda, I. \u010cern\u00e1, L. Sekanina, T. Vojnar, D. Anto\u0161. Lecture Notes in Computer Science, vol. 7119 (Springer, Heidelberg, 2012), pp. 47\u201356","DOI":"10.1007\/978-3-642-25929-6_4"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, The theory of hybrid automata, in Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (1996), pp. 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"1_CR14","unstructured":"M.A. Heroux, D.W. Doerfler, P.S. Crozier, J.M. Willenbring, C. Edwards, A. Williams, M. Rajan, E.R. Keiter, H.K. Thornquist, R.W. Numrich, Improving performance via mini-applications. Report SAND2009-5574, Sandia National Laboratories (2009)"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.entcs.2015.10.008","volume":"317","author":"GC Hulette","year":"2015","unstructured":"G.C. Hulette, R.C. Armstrong, J.R. Mayo, J.R. Ruthruff, Theorem-proving analysis of digital control logic interacting with continuous dynamics. Electron. Notes Theor. Comput. Sci. 317, 71\u201383 (2015)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"M. Jackson, P. Zave, Deriving specifications from requirements: an example, in Proceedings of the 17th International Conference on Software Engineering (1995), pp. 15\u201324","DOI":"10.1145\/225014.225016"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"A. Joshi, S.P. Miller, M. Whalen, M.P. Heimdahl, A proposal for model-based safety analysis, in Proceedings of the 24th Digital Avionics Systems Conference (2005)","DOI":"10.1109\/DASC.2005.1563469"},{"key":"1_CR18","unstructured":"A. Joshi, M.P.E. Heimdahl, S.P. Miller, M.W. Whalen, Model-based safety analysis. NASA Contractor Report CR-2006-213953 (2006)"},{"key":"1_CR19","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195079517.001.0001","volume-title":"The Origins of Order: Self-organization and Selection in Evolution","author":"SA Kauffman","year":"1993","unstructured":"S.A. Kauffman, The Origins of Order: Self-organization and Selection in Evolution (Oxford University Press, Oxford, 1993)"},{"key":"1_CR20","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (Addison-Wesley, Boston, 2002)"},{"issue":"8","key":"1_CR21","doi-asserted-by":"publisher","first-page":"1056","DOI":"10.1007\/s10701-012-9647-7","volume":"42","author":"L Lamport","year":"2012","unstructured":"L. Lamport, Buridan\u2019s principle. Found. Phys. 42(8), 1056\u20131066 (2012)","journal-title":"Found. Phys."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"J.R. Mayo, R.C. Armstrong, G.C. Hulette, Digital system robustness via design constraints: the lesson of formal methods, in Proceedings of the 9th Annual IEEE International Systems Conference (2015), pp. 109\u2013114","DOI":"10.1109\/SYSCON.2015.7116737"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"J.R. Mayo, R.C. Armstrong, G.C. Hulette, Leveraging abstraction to establish out-of-nominal safety properties, in Proceedings of the 4th International Workshop on Formal Techniques for Safety-Critical Systems, ed. by C. Artho, P.C. \u00d6lveczky. Communications in Computer and Information Science, vol. 596 (Springer, Heidelberg, 2016), pp. 172\u2013186","DOI":"10.1007\/978-3-319-29510-7_10"},{"key":"1_CR24","doi-asserted-by":"publisher","DOI":"10.1063\/1.3187791","volume":"19","author":"T Mytkowicz","year":"2009","unstructured":"T. Mytkowicz, A. Diwan, E. Bradley, Computer systems are dynamical systems. Chaos 19, 033124 (2009)","journal-title":"Chaos"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"A. Platzer, J.D. Quesel, KeYmaera: a hybrid theorem prover for hybrid systems, in Automated Reasoning, ed. by A. Armando, P. Baumgartner, G. Dowek. Lecture Notes in Computer Science, vol. 5195 (Springer, Heidelberg, 2008), pp. 171\u2013178","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"1_CR26","unstructured":"J. Ray, J.R. Mayo, R.C. Armstrong, Finite difference stencils robust to silent data corruption, in SIAM Conference on Parallel Processing for Scientific Computing (2014). https:\/\/www.pathlms.com\/siam\/courses\/477\/sections\/716"},{"issue":"2","key":"1_CR27","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"HG Rice","year":"1953","unstructured":"H.G. Rice, Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74(2), 358\u2013366 (1953)","journal-title":"Trans. Am. Math. Soc."},{"key":"1_CR28","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718003","volume-title":"Iterative Methods for Sparse Linear Systems","author":"Y Saad","year":"2003","unstructured":"Y. Saad, Iterative Methods for Sparse Linear Systems, 2nd edn. (SIAM, Philadelphia, 2003)","edition":"2"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"M. Salloum, J.R. Mayo, R.C. Armstrong, In-situ mitigation of silent data corruption in PDE solvers, in Proceedings of the 6th Workshop on Fault Tolerance for HPC at Extreme Scale (2016)","DOI":"10.1145\/2909428.2909433"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"M.U. Sanwal, O. Hasan, Formal verification of cyber-physical systems: coping with continuous elements, in ICCSA\u201913, ed. by B. Murgante, S. Misra, M. Carlini, C.M. Torre, H.Q. Nguyen, D. Taniar, B.O. Apduhan, O. Gervasi. Lecture Notes in Computer Science, vol. 7971 (Springer, Heidelberg, 2013), pp. 358\u2013371","DOI":"10.1007\/978-3-642-39637-3_29"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"S.A. Seshia, W. Li, S. Mitra, Verification-guided soft error resilience, in Proceedings of the Conference on Design, Automation and Test in Europe (2007), pp. 1442\u20131447","DOI":"10.1109\/DATE.2007.364501"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"P. Strazdins, B. Harding, C. Lee, J.R. Mayo, J. Ray, R.C. Armstrong, A robust technique to make a 2D advection solver tolerant to soft faults, in Proceedings of the International Conference on Computational Science (2016)","DOI":"10.1016\/j.procs.2016.05.505"},{"key":"1_CR33","unstructured":"The Coq development team, The Coq proof assistant reference manual (2004). http:\/\/coq. inria.fr"},{"key":"1_CR34","unstructured":"O. Tveretina, Towards the safety verification of real-time systems with the Coq proof assistant, in Proceedings of the International Multiconference on Computer Science and Information Technology, vol. 2 (2007), pp. 883\u2013892"},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"J. Woodcock, P.G. Larsen, J. Bicarregui, J. Fitzgerald, Formal methods: practice and experience. ACM Comput. Surv. 41, 19 (2009)","journal-title":"ACM Comput. Surv."}],"container-title":["Cyber-Physical Systems Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98935-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,13]],"date-time":"2024-07-13T02:59:15Z","timestamp":1720839555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98935-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989341","9783319989358"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98935-8_1","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}