[{"date_created":"2018-12-11T12:09:34Z","date_published":"2005-03-24T00:00:00Z","extern":"1","year":"2005","status":"public","intvolume":"      3442","type":"conference","conference":{"start_date":"2005-04-04","end_date":"2005-04-08","name":"FASE: Fundamental Approaches To Software Engineering","location":"Edinburgh, United Kingdom"},"publist_id":"131","fulldoi":"https://doi.org/10.1007/978-3-540-31984-9_2","publication_status":"published","publication":"Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software Engineering","volume":3442,"OA_type":"closed access","author":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"Dirk"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Ranjit","full_name":"Jhala, Ranjit","last_name":"Jhala"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"day":"24","page":"2 - 18","title":"Checking memory safety with BLAST","date_updated":"2026-09-30T14:10:19Z","publisher":"Springer Nature","_id":"4579","acknowledgement":"This research was supported in part by the NSF grants CCR-0234690, CCR-0225610, and ITR-0326577.","alternative_title":["LNCS"],"article_processing_charge":"No","abstract":[{"lang":"eng","text":"BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use Ccured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by Ccured and provide useful information to the programmer about many of the remaining checks."}],"publication_identifier":{"isbn":["9783540254201"]},"citation":{"ama":"Beyer D, Henzinger TA, Jhala R, Majumdar R. Checking memory safety with BLAST. In: <i>Proceedings of the 8th International Conference, Held as Part of the Joint European Conference on Theory and Practice of Software Conference on Fundamental Approaches to Software Engineering</i>. Vol 3442. Springer Nature; 2005:2-18. doi:<a href=\"https://doi.org/10.1007/978-3-540-31984-9_2\">10.1007/978-3-540-31984-9_2</a>","chicago":"Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “Checking Memory Safety with BLAST.” In <i>Proceedings of the 8th International Conference, Held as Part of the Joint European Conference on Theory and Practice of Software Conference on Fundamental Approaches to Software Engineering</i>, 3442:2–18. Springer Nature, 2005. <a href=\"https://doi.org/10.1007/978-3-540-31984-9_2\">https://doi.org/10.1007/978-3-540-31984-9_2</a>.","short":"D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the 8th International Conference, Held as Part of the Joint European Conference on Theory and Practice of Software Conference on Fundamental Approaches to Software Engineering, Springer Nature, 2005, pp. 2–18.","ista":"Beyer D, Henzinger TA, Jhala R, Majumdar R. 2005. Checking memory safety with BLAST. Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches To Software Engineering, LNCS, vol. 3442, 2–18.","ieee":"D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “Checking memory safety with BLAST,” in <i>Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software Engineering</i>, Edinburgh, United Kingdom, 2005, vol. 3442, pp. 2–18.","apa":"Beyer, D., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2005). Checking memory safety with BLAST. In <i>Proceedings of the 8th international conference, held as part of the joint European Conference on Theory and Practice of Software conference on Fundamental Approaches to Software Engineering</i> (Vol. 3442, pp. 2–18). Edinburgh, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-540-31984-9_2\">https://doi.org/10.1007/978-3-540-31984-9_2</a>","mla":"Beyer, Dirk, et al. “Checking Memory Safety with BLAST.” <i>Proceedings of the 8th International Conference, Held as Part of the Joint European Conference on Theory and Practice of Software Conference on Fundamental Approaches to Software Engineering</i>, vol. 3442, Springer Nature, 2005, pp. 2–18, doi:<a href=\"https://doi.org/10.1007/978-3-540-31984-9_2\">10.1007/978-3-540-31984-9_2</a>."},"doi":"10.1007/978-3-540-31984-9_2","month":"03","language":[{"iso":"eng"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"None"}]