{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:58:01Z","timestamp":1743109081247,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214092"},{"type":"electronic","value":"9783319214108"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21410-8_46","type":"book-chapter","created":{"date-parts":[[2015,6,18]],"date-time":"2015-06-18T15:57:14Z","timestamp":1434643034000},"page":"597-611","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Novel Designs for Memory Checkers Using Semantics and Digital Sequential Circuits"],"prefix":"10.1007","author":[{"given":"Mohamed A.","family":"El-Zawawy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,6,19]]},"reference":[{"key":"46_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Dwarkadas, S., Rezine, A., Shriraman, A., Zhu, Y.: Verifying safety and liveness for the flextm hybrid transactional memory. In: Macii, E. (ed.) Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18\u201322, 2013, pp. 785\u2013790. EDA Consortium San Jose, CA, USA \/ ACM DL (2013)","DOI":"10.7873\/DATE.2013.167"},{"key":"46_CR2","doi-asserted-by":"crossref","unstructured":"Austin, T.M., Breach, S.E., Sohi, G.S.: Efficient detection of all pointer and array access errors. In: Sarkar, V., Ryder, B.G., Soffa, M.L. (eds.) PLDI, pp. 290\u2013301. ACM (1994)","DOI":"10.1145\/773473.178446"},{"issue":"12","key":"46_CR3","doi-asserted-by":"publisher","first-page":"1572","DOI":"10.1002\/cpe.1391","volume":"21","author":"J Baker","year":"2009","unstructured":"Baker, J., Cunei, A., Kalibera, T., Pizlo, F., Vitek, J.: Accurate garbage collection in uncooperative environments revisited. Concurrency and Computation: Practice and Experience 21(12), 1572\u20131606 (2009)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"46_CR4","unstructured":"Bensalem, S., Peled, D. (eds): Runtime Verification. 9th International Workshop, RV 2009, Grenoble, France, June 26\u201328, 2009. Selected Papers, volume 5779 of Lecture Notes in Computer Science. Springer (2009)"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"Berger, E.D., Zorn, B.G.: Diehard: probabilistic memory safety for unsafe languages. In: Schwartzbach, M.I., Ball, T. (eds) PLDI, pp. 158\u2013168. ACM (2006)","DOI":"10.1145\/1133255.1134000"},{"key":"46_CR6","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.ic.2013.04.003","volume":"228","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Prabhu, V.S.: Synthesis of memory-efficient, clock-memory free, and non-zeno safety controllers for timed systems. Inf. Comput. 228, 83\u2013119 (2013)","journal-title":"Inf. Comput."},{"key":"46_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-13754-9_6","volume-title":"Time for Verification","author":"W Damm","year":"2010","unstructured":"Damm, W., Dierks, H., Oehlerking, J., Pnueli, A.: Towards Component Based Design of Hybrid Systems: Safety and Stability. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 96\u2013143. Springer, Heidelberg (2010)"},{"key":"46_CR8","unstructured":"Dhurjati, D., Adve, V.S.: Efficiently detecting all dangling pointer uses in production servers. In: DSN, pp. 269\u2013280. IEEE Computer Society (2006)"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"Dhurjati, D., Kowshik, S., Adve, V.S., Lattner, C.: Memory safety without runtime checks or garbage collection. In: Mueller, F., Kremer, U. (eds.) LCTES, pp. 69\u201380. ACM (2003)","DOI":"10.1145\/780731.780743"},{"key":"46_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-319-08867-9_32","volume-title":"Computer Aided Verification","author":"T Dillig","year":"2014","unstructured":"Dillig, T., Dillig, I., Chaudhuri, S.: Optimal guard synthesis for memory safety. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 491\u2013507. Springer, Heidelberg (2014)"},{"key":"46_CR11","unstructured":"Godefroid, P., Kinder, J.: Proving memory safety of floating-point computations by combining static and dynamic program analysis. In: Tonella, P., Orso, A. (eds.), Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, July 12\u201316, 2010, pp. 1\u201312. ACM (2010)"},{"key":"46_CR12","doi-asserted-by":"crossref","unstructured":"Grossman, D., Morrisett, J.G., Jim, T., Hicks, M.W., Wang, Y., Cheney, J.: Region-based memory management in cyclone. In: Knoop, J., Hendren, L.J. (eds.) PLDI, pp. 282\u2013293. ACM (2002)","DOI":"10.1145\/543552.512563"},{"key":"46_CR13","doi-asserted-by":"crossref","unstructured":"Hertz, M., Berger, E.D.: Quantifying the performance of garbage collection vs. explicit memory management. In: Johnson, R.E., Gabriel, R.P. (eds.) OOPSLA, pp. 313\u2013326. ACM (2005)","DOI":"10.1145\/1103845.1094836"},{"key":"46_CR14","unstructured":"Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of c. In: Ellis, C.S. (ed.) USENIX Annual Technical Conference, General Track, pages 275\u2013288. USENIX (2002)"},{"key":"46_CR15","volume-title":"Theory of Recursive Functions and Effective Computability","author":"H Rogers Jr","year":"1987","unstructured":"Rogers Jr, H.: Theory of Recursive Functions and Effective Computability. MIT press, Cambridge, MA (1987)"},{"key":"46_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF00289062","volume":"14","author":"L Lamport","year":"1980","unstructured":"Lamport, L.: The hoare logic\u2019 of concurrent programs. Acta Inf. 14, 21\u201337 (1980)","journal-title":"Acta Inf."},{"issue":"11","key":"46_CR17","doi-asserted-by":"publisher","first-page":"1796","DOI":"10.1016\/j.ress.2009.05.012","volume":"94","author":"H-C Lee","year":"2009","unstructured":"Lee, H.-C., Seong, P.-H.: A computational model for evaluating the effects of attention, memory, and mental models on situation assessment of nuclear power plant operators. Rel. Eng. & Sys. Safety 94(11), 1796\u20131805 (2009)","journal-title":"Rel. Eng. & Sys. Safety"},{"issue":"7","key":"46_CR18","doi-asserted-by":"publisher","first-page":"1825","DOI":"10.1016\/j.automatica.2014.04.006","volume":"50","author":"H Li","year":"2014","unstructured":"Li, H., Gao, H., Shi, P., Zhao, X.: Fault-tolerant control of markovian jump stochastic systems via the augmented sliding mode observer approach. Automatica 50(7), 1825\u20131834 (2014)","journal-title":"Automatica"},{"key":"46_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-319-06410-9_32","volume-title":"FM 2014: Formal Methods","author":"C Marriott","year":"2014","unstructured":"Marriott, C., Cavalcanti, A.: SCJ: memory-safety checking without annotations. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 465\u2013480. Springer, Heidelberg (2014)"},{"key":"46_CR20","doi-asserted-by":"crossref","unstructured":"Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Watchdog: Hardware for safe and secure manual memory management and full memory safety. In: 39th International Symposium on Computer Architecture (ISCA 2012), June 9\u201313, 2012, Portland, OR, USA, pp. 189\u2013200. IEEE (2012)","DOI":"10.1109\/ISCA.2012.6237017"},{"issue":"3","key":"46_CR21","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1145\/1065887.1065892","volume":"27","author":"GC Necula","year":"2005","unstructured":"Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: Ccured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. 27(3), 477\u2013526 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"46_CR22","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: Ccured: type-safe retrofitting of legacy code. In: Launchbury, J., Mitchell, J.C. (eds.) POPL, pp. 128\u2013139. ACM (2002)","DOI":"10.1145\/565816.503286"},{"key":"46_CR23","doi-asserted-by":"crossref","unstructured":"Oiwa, Y.: Implementation of the memory-safe full ansi-c compiler. In: Hind, M., Diwan, A. (eds) PLDI, pp. 259\u2013269. ACM (2009)","DOI":"10.1145\/1543135.1542505"},{"issue":"1","key":"46_CR24","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1002\/(SICI)1097-024X(199701)27:1<87::AID-SPE78>3.0.CO;2-P","volume":"27","author":"H Patil","year":"1997","unstructured":"Patil, H., Fischer, C.N.: Low-cost, concurrent checking of pointer and array accesses in c programs. Softw., Pract. Exper. 27(1), 87\u2013110 (1997)","journal-title":"Softw., Pract. Exper."},{"key":"46_CR25","doi-asserted-by":"crossref","unstructured":"Qin, F., Tucek, J., Zhou, Y., Sundaresan, J.: Rx: Treating bugs as allergies - a safe method to survive software failures. ACM Trans. Comput. Syst. 25(3) (2007)","DOI":"10.1145\/1275517.1275519"},{"key":"46_CR26","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22\u201325 July 2002, Copenhagen, Denmark, Proceedings, pp. 55\u201374. IEEE Computer Society (2002)"},{"key":"46_CR27","unstructured":"Rinard, M.C., Cadar, C., Dumitran, D., Roy, D.M., Leu,T., Beebee, W.S.: Enhancing server availability and security through failure-oblivious computing. In: Brewer, E.A., Chen, P. (eds.) OSDI, pp. 303\u2013316. USENIX Association (2004)"},{"key":"46_CR28","doi-asserted-by":"crossref","unstructured":"Rosu, G., Schulte, W., Serbanuta, T.-F.: Runtime verification of c memory safety. In: Bensalem and Peled [4], pp. 132\u2013151","DOI":"10.1007\/978-3-642-04694-0_10"},{"issue":"1","key":"46_CR29","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1002\/spe.2105","volume":"43","author":"MS Simpson","year":"2013","unstructured":"Simpson, M.S., Barua, R.: Memsafe: ensuring the spatial and temporal memory safety of c at runtime. Softw., Pract. Exper. 43(1), 93\u2013128 (2013)","journal-title":"Softw., Pract. Exper."},{"issue":"3","key":"46_CR30","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/MM.2013.50","volume":"33","author":"A Singh","year":"2013","unstructured":"Singh, A., Narayanasamy, S., Marino, D., Millstein, T.D., Musuvathi, M.: A safety-first approach to memory models. IEEE Micro 33(3), 96\u2013104 (2013)","journal-title":"IEEE Micro"},{"key":"46_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-319-08587-6_15","volume-title":"Automated Reasoning","author":"T Str\u00f6der","year":"2014","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 208\u2013223. Springer, Heidelberg (2014)"},{"key":"46_CR32","unstructured":"Vazou, N., Papakyriakou, M.A., Papaspyrou, N.: Memory safety and race freedom in concurrent programming languages with linear capabilities. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Federated Conference on Computer Science and Information Systems - FedCSIS 2011, Szczecin, Poland, 18\u201321 September 2011, Proceedings, pp. 833\u2013840 (2011)"},{"key":"46_CR33","doi-asserted-by":"crossref","unstructured":"Xu, W., DuVarney, D.C., Sekar, R.: An efficient and backwards-compatible transformation to ensure memory safety of c programs. In: Taylor, R.N., Dwyer, M.B. (eds.) SIGSOFT FSE, pp. 117\u2013126. ACM (2004)","DOI":"10.1145\/1041685.1029913"},{"issue":"3","key":"46_CR34","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/2500875","volume":"57","author":"J Yang","year":"2014","unstructured":"Yang, J., Cui, H., Jingyue, W., Tang, Y., Gang, H.: Making parallel programs reliable with stable multithreading. Commun. ACM 57(3), 58\u201369 (2014)","journal-title":"Commun. ACM"},{"key":"46_CR35","doi-asserted-by":"crossref","unstructured":"Yong, S.H., Horwitz, S.: Protecting c programs from attacks via invalid pointer dereferences. In: ESEC \/ SIGSOFT FSE, pp. 307\u2013316. ACM (2003)","DOI":"10.1145\/949952.940113"},{"issue":"7","key":"46_CR36","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1002\/spe.4380230704","volume":"23","author":"BG Zorn","year":"1993","unstructured":"Zorn, B.G.: The measured cost of conservative garbage collection. Softw., Pract. Exper. 23(7), 733\u2013756 (1993)","journal-title":"Softw., Pract. Exper."}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications -- ICCSA 2015"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21410-8_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:36:14Z","timestamp":1676946974000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21410-8_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214092","9783319214108"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21410-8_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}