{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T00:40:05Z","timestamp":1743727205609,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642317613"},{"type":"electronic","value":"9783642317620"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-31762-0_6","type":"book-chapter","created":{"date-parts":[[2012,7,11]],"date-time":"2012-07-11T10:09:11Z","timestamp":1342001351000},"page":"67-85","source":"Crossref","is-referenced-by-count":2,"title":["Modeling and Analyzing the Interaction of C and C++ Strings"],"prefix":"10.1007","author":[{"given":"Gogul","family":"Balakrishnan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoto","family":"Maeda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rakesh","family":"Pothengil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Coverity Inc. program verifier, www.coverity.com","key":"6_CR1"},{"unstructured":"GrammaTech CodeSonar, www.grammatech.com\/products\/codesonar","key":"6_CR2"},{"unstructured":"PolySpace program analysis tool, www.polyspace.com","key":"6_CR3"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11823230_4","volume-title":"Static Analysis","author":"X. Allamigeon","year":"2006","unstructured":"Allamigeon, X., Godard, W., Hymans, C.: Static Analysis of String Manipulations in Critical Embedded C Programs. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 35\u201351. Springer, Heidelberg (2006)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-73368-3_41","volume-title":"Computer Aided Verification","author":"D. Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural Abstraction of Software Verification Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 366\u2013378. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI 2001, pp. 203\u2013213. ACM Press (2001)","key":"6_CR6","DOI":"10.1145\/381694.378846"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, vol.\u00a0548030, pp. 196\u2013207. ACM Press (June 2003)","key":"6_CR8","DOI":"10.1145\/780822.781153"},{"doi-asserted-by":"crossref","unstructured":"Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: preventing data races and deadlocks. In: OOPSLA, pp. 211\u2013230 (2002)","key":"6_CR9","DOI":"10.1145\/583854.582440"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A Reachability Predicate for Analyzing Low-Level Software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"A. Christensen","year":"2003","unstructured":"Christensen, A., M\u00f8ller, A., Schwartzbach, M.: Precise Analysis of String Expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA, pp. 48\u201364 (1998)","key":"6_CR12","DOI":"10.1145\/286942.286947"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Intl. Symp. on Programming, Dunod, France, pp. 106\u2013130 (1976)","key":"6_CR15","DOI":"10.1145\/390018.808314"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977)","key":"6_CR16","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: POPL, pp. 84\u201397. ACM (January 1978)","key":"6_CR17","DOI":"10.1145\/512760.512770"},{"unstructured":"Cowan, C., Wagle, P., Pu, C., Beattie, S., Walpole, J.: Buffer overflows: Attacks and defenses for the vulnerability of the decade. In: Proc. DARPA Information Survivability Conference and Expo. (DISCEX). IEEE (1999)","key":"6_CR18"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11823230_1","volume-title":"Static Analysis","author":"M. Das","year":"2006","unstructured":"Das, M.: Unleashing the Power of Static Analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 1\u20132. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: PLDI, pp. 57\u201368. ACM Press (2002)","key":"6_CR20","DOI":"10.1145\/543552.512538"},{"doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL, pp. 187\u2013200. ACM (2011)","key":"6_CR21","DOI":"10.1145\/1925844.1926407"},{"doi-asserted-by":"crossref","unstructured":"Dor, N., Rodeh, M., Sagiv, M.: CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. In: Proc. PLDI. ACM Press (2003)","key":"6_CR22","DOI":"10.1145\/781131.781149"},{"doi-asserted-by":"crossref","unstructured":"Heine, D.L., Lam, M.S.: A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In: PLDI, pp. 168\u2013181. ACM (2003)","key":"6_CR23","DOI":"10.1145\/780822.781150"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","key":"6_CR24","DOI":"10.1145\/565816.503279"},{"doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Balakrishnan, G., Gupta, A., Sankaranarayanan, S., Maeda, N., Tokuoka, H., Imoto, T., Miyazaki, Y.: DC2: A framework for scalable, scope-bounded software verification. In: ASE (2011)","key":"6_CR25","DOI":"10.1109\/ASE.2011.6100046"},{"doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A., Ganai, M., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: ICCD, pp. 297\u2013308. IEEE (2005)","key":"6_CR26","DOI":"10.1109\/ICCD.2005.77"},{"doi-asserted-by":"crossref","unstructured":"Kurshan, R.: Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. Princeton University Press (1994)","key":"6_CR27","DOI":"10.1515\/9781400864041"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A New Numerical Abstract Domain Based on Difference-Bound Matrices. In: Danvy, O., Filinski, A. (eds.) PADO II. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, IEEE, pp. 310\u2013319. IEEE CS Press (October 2001)","key":"6_CR29","DOI":"10.1109\/WCRE.2001.957836"},{"unstructured":"Moy, Y.: Automatic Modular Static Safety Checking for C Programs. PhD thesis, Universit\u00e9 Paris-Sud (January 2009)","key":"6_CR30"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-642-22655-7_27","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"P. Prabhu","year":"2011","unstructured":"Prabhu, P., Maeda, N., Balakrishnan, G., Ivan\u010di\u0107, F., Gupta, A.: Interprocedural Exception Analysis for C++. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol.\u00a06813, pp. 583\u2013608. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Rugina, R., Rinard, M.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In: PLDI, pp. 182\u2013195. ACM (2000)","key":"6_CR33","DOI":"10.1145\/358438.349325"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/978-3-642-05089-3_48","volume-title":"FM 2009: Formal Methods","author":"D. Shao","year":"2009","unstructured":"Shao, D., Khurshid, S., Perry, D.E.: An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 757\u2013772. Springer, Heidelberg (2009)"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45719-4_25","volume-title":"Algebraic Methodology and Software Technology","author":"A. Simon","year":"2002","unstructured":"Simon, A., King, A.: Analyzing String Buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 365\u2013379. Springer, Heidelberg (2002)"},{"unstructured":"Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Proc. Network and Distributed Systems Security Conference, pp. 3\u201317. ACM Press (2000)","key":"6_CR36"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-642-28652-0_8","volume-title":"Compiler Construction","author":"J. Yang","year":"2012","unstructured":"Yang, J., Balakrishnan, G., Maeda, N., Ivan\u010di\u0107, F., Gupta, A., Sinha, N., Sankaranarayanan, S., Sharma, N.: Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis. In: O\u2019Boyle, M. (ed.) CC 2012. LNCS, vol.\u00a07210, pp. 144\u2013164. Springer, Heidelberg (2012)"},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-12002-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Yu","year":"2010","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: An Automata-Based String Analysis Tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 154\u2013157. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31762-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T21:13:58Z","timestamp":1743714838000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31762-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642317613","9783642317620"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31762-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}