{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T13:10:02Z","timestamp":1746364202512,"version":"3.40.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105055"},{"type":"electronic","value":"9783319105062"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-10506-2_14","type":"book-chapter","created":{"date-parts":[[2014,9,3]],"date-time":"2014-09-03T02:41:50Z","timestamp":1409712110000},"page":"202-213","source":"Crossref","is-referenced-by-count":12,"title":["Proving the Absence of Stack Overflows"],"prefix":"10.1007","author":[{"given":"Daniel","family":"K\u00e4stner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Ferdinand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"AbsInt. AIS Quick Reference Guide (2013)"},{"key":"14_CR2","unstructured":"AbsInt. XTC Language Specification Version 2.1 (2013), http:\/\/www.absint.com\/xtc\/"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/1023833.1023872","volume-title":"Proceedings of the 2004 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES 2004","author":"S. Biswas","year":"2004","unstructured":"Biswas, S., Simpson, M., Barua, R.: Memory overflow protection for embedded systems using run-time checks, reuse and compression. In: Proceedings of the 2004 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES 2004, pp. 280\u2013291. ACM, New York (2004)"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1109\/ICSE.2001.919080","volume-title":"Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001","author":"D. Brylow","year":"2001","unstructured":"Brylow, D., Damgaard, N., Palsberg, J.: Static checking of interrupt-driven software. In: Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, pp. 47\u201356. IEEE Computer Society Press, Washington, DC (2001)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/3-540-44898-5_7","volume-title":"Static Analysis","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T.A., Palsberg, J.: Stack size analysis for interrupt-driven programs. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 109\u2013126. Springer, Heidelberg (2003)"},{"key":"14_CR6","first-page":"238","volume-title":"POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"14_CR7","unstructured":"Dunn, M.: Toyota\u2019s killer firmware: Bad design and its consequences. EDN Network (October 2013), http:\/\/www.edn.com\/design\/automotive\/4423428\/Toyota-s-killer-firmware--Bad-design-and-its-consequences"},{"key":"14_CR8","first-page":"20","volume-title":"Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC 2000","author":"R.S. Engelschall","year":"2000","unstructured":"Engelschall, R.S.: Portable multithreading: The signal stack trick for user-space thread creation. In: Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC 2000, p. 20. USENIX Association, Berkeley (2000)"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1109\/COMPSAC.2013.100","volume-title":"Proceedings of the 2013 IEEE 37th Annual Computer Software and Applications Conference, COMPSAC 2013","author":"M. Eslamimehr","year":"2013","unstructured":"Eslamimehr, M., Palsberg, J.: Testing versus static analysis of maximum stack size. In: Proceedings of the 2013 IEEE 37th Annual Computer Software and Applications Conference, COMPSAC 2013, pp. 619\u2013626. IEEE Computer Society Press, Washington, DC (2013)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Ferdinand, C.: Cache Behavior Prediction for Real-Time Systems. PhD thesis, Saarland University (1997)","DOI":"10.1007\/BFb0057777"},{"key":"14_CR11","unstructured":"Ferdinand, C., Heckmann, R., Franzen, B.: Static Memory and Timing Analysis of Embedded Systems Code. In: Groot, P. (ed.) Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007), Eindhoven, The Netherlands, March 23. TUE Computer Science Reports, vol.\u00a007-04 (2007)"},{"key":"14_CR12","unstructured":"Ferdinand, C., Heckmann, R., Le Sergent, T., Lopes, D., Martin, B., Fornari, X., Martin, F.: Combining a high-level design tool for safety-critical systems with a tool for WCET analysis on executables. In: 4th European Congress ERTS Embedded Real Time Software, Toulouse, France (January 2008)"},{"key":"14_CR13","unstructured":"Guillemin, P.: Stack overflow detection using the ST9 timer\/watchdog. Doc id 2476 rev 2, STMicroelectronics (2011)"},{"key":"14_CR14","unstructured":"Heckmann, R., Ferdinand, C.: Stack Usage Analysis and Software Visualization for Embedded Processors. In: Grote, C. (ed.) Vortr\u00e4ge und Begleittexte zur Embedded Intelligence 2002. Grundlagen, Architekturen, Werkzeuge und L\u00f6sungen, N\u00fcrnberg, Poing, Februar 19-21. Design & Elektronik (2002)"},{"issue":"5","key":"14_CR15","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/378995.379006","volume":"28","author":"J. Hill","year":"2000","unstructured":"Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. SIGARCH Comput. Archit. News\u00a028(5), 93\u2013104 (2000)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"14_CR16","unstructured":"K\u00e4stner, D., Kiffmeier, U., Fleischer, D., Nenova, S., Schlickling, M., Ferdinand, C.: Integrating Model-Based Code Generators with Static Program Analyzers. Embedded World Congress (2013)"},{"key":"14_CR17","unstructured":"K\u00e4stner, D., Pister, M., Gebhard, G., Schlickling, M., Ferdinand, C.: Confidence in Timing. In: Safecomp 2013 Workshop: Next Generation of System Assurance Approaches for Safety-Critical Systems, SASSUR (September 2013)"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-69830-2_19","volume-title":"Wireless Sensor Networks","author":"H. Kim","year":"2007","unstructured":"Kim, H., Cha, H.: Multithreading optimization techniques for sensor network operating systems. In: Langendoen, K.G., Voigt, T. (eds.) EWSN 2007. LNCS, vol.\u00a04373, pp. 293\u2013308. Springer, Heidelberg (2007)"},{"key":"14_CR19","unstructured":"Min\u00e9, A.: Weakly Relational Numerical Abstract Domains. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (December 2004), http:\/\/www.di.ens.fr\/~mine\/these\/these-color.pdf"},{"key":"14_CR20","unstructured":"OSEK\/VDX. OSEK\/VDX Operating System. Version 2.2.3 (2005)"},{"key":"14_CR21","series-title":"SCI","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-642-21375-5_10","volume-title":"Computers,Networks, Systems, and Industrial Engineering 2011","author":"S.H. Park","year":"2011","unstructured":"Park, S.H., Lee, D.K., Kang, S.J.: Compiler-assisted maximum stack usage measurement technique for efficient multi-threading in memory-limited embedded systems. In: Lee, R. (ed.) Computers,Networks, Systems, and Industrial Engineering 2011. SCI, vol.\u00a0365, pp. 113\u2013129. Springer, Heidelberg (2011)"},{"key":"14_CR22","unstructured":"Radio Technical Commission for Aeronautics. RTCA DO-178B. Software Considerations in Airborne Systems and Equipment Certification (1992)"},{"key":"14_CR23","unstructured":"Real Time Engineers Ltd. FreeRTOSTM web page: Stack Usage and Stack Overflow Checking (2010), http:\/\/www.freertos.org\/Stacks-and-stack-overflow-checking.html"},{"key":"14_CR24","first-page":"290","volume-title":"Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT 2005","author":"J. Regehr","year":"2005","unstructured":"Regehr, J.: Random testing of interrupt-driven software. In: Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT 2005, pp. 290\u2013298. ACM, New York (2005)"},{"issue":"4","key":"14_CR25","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1145\/1113830.1113833","volume":"4","author":"J. Regehr","year":"2005","unstructured":"Regehr, J., Reid, A., Webb, K.: Eliminating stack overflow by abstract interpretation. ACM Trans. Embed. Comput. Syst.\u00a04(4), 751\u2013778 (2005)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Theiling, H.: Extracting Safe and Precise Control Flow from Binaries. In: Proceedings of the 7th Conference on Real-Time Computing and Applications Symposium (RTCSA 2000), Cheju Island, South Korea, December 12-14, pp. 23\u201330. IEEE Computer Society Press (2000)","DOI":"10.1109\/RTCSA.2000.896367"},{"key":"14_CR27","unstructured":"Thesing, S.: Safe and Precise WCET Determinations by Abstract Interpretation of Pipeline Models. PhD thesis, Saarland University (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10506-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T12:51:47Z","timestamp":1746363107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10506-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319105055","9783319105062"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10506-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}