{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T00:04:36Z","timestamp":1743120276253,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319681665"},{"type":"electronic","value":"9783319681672"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_2","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"25-41","source":"Crossref","is-referenced-by-count":5,"title":["Precise Null Pointer Analysis Through Global Value Numbering"],"prefix":"10.1007","author":[{"given":"Ankush","family":"Das","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"2_CR1","unstructured":"Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, DIKU, University of Copenhagen, May 1994"},{"key":"2_CR2","unstructured":"Barnett, M., Qadeer, S.: BCT: A translator from MSIL to Boogie. In: Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (2012)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Choi, J.D., Burke, M., Carini, P.: Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In: Principles of Programming Languages, pp. 232\u2013245 (1993)","DOI":"10.1145\/158511.158639"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Cocke, J.: Global common subexpression elimination. In: Proceedings of a Symposium on Compiler Optimization, pp. 20\u201324. ACM, New York (1970)","DOI":"10.1145\/800028.808480"},{"issue":"4","key":"2_CR5","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-319-21690-4_19","volume-title":"Computer Aided Verification","author":"A Das","year":"2015","unstructured":"Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324\u2013342. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21690-4_19"},{"key":"2_CR7","unstructured":"Das, A., Lal, A.: Precise null pointer analysis through global value numbering. CoRR abs\/1702.05807 (2017). \nhttp:\/\/arxiv.org\/abs\/1702.05807"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-31057-7_29","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"A De","year":"2012","unstructured":"De, A., D\u2019Souza, D.: Scalable flow-sensitive pointer analysis for java with strong updates. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 665\u2013687. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-31057-7_29"},{"issue":"2","key":"2_CR9","first-page":"9:1","volume":"17","author":"SJ Fink","year":"2008","unstructured":"Fink, S.J., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol. 17(2), 9:1\u20139:34 (2008)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Necula, G.C.: Global value numbering using random interpretation. In: Principles of Programming Languages, POPL, pp. 342\u2013352 (2004)","DOI":"10.1145\/964001.964030"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Hardekopf, B., Lin, C.: Flow-sensitive pointer analysis for millions of lines of code. In: Code Generation and Optimization (CGO), pp. 289\u2013298 (2011)","DOI":"10.1109\/CGO.2011.5764696"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Hasti, R., Horwitz, S.: Using static single assignment form to improve flow-insensitive pointer analysis. In: Programming Language Design and Implementation (PLDI), pp. 97\u2013105 (1998)","DOI":"10.1145\/277650.277668"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: Programming Language Design and Implementation (PLDI), pp. 24\u201334 (2001)","DOI":"10.1145\/378795.378802"},{"issue":"1","key":"2_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/239912.239913","volume":"19","author":"S Horwitz","year":"1997","unstructured":"Horwitz, S.: Precise flow-insensitive may-alias analysis is NP-Hard. ACM Trans. Program. Lang. Syst. 19(1), 1\u20136 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: Principles of Programming Languages (POPL), pp. 66\u201374 (1982)","DOI":"10.1145\/582153.582161"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Principles of Programming Languages, pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Powering the static driver verifier using corral. In: Foundations of Software Engineering, pp. 202\u2013212 (2014)","DOI":"10.1145\/2635868.2635894"},{"issue":"4","key":"2_CR18","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1145\/989393.989440","volume":"39","author":"W Landi","year":"2004","unstructured":"Landi, W., Ryder, B.G.: A safe approximate algorithm for interprocedural pointer aliasing. SIGPLAN Not. 39(4), 473\u2013489 (2004)","journal-title":"SIGPLAN Not."},{"key":"2_CR19","unstructured":"Leino, K.R.M.: This is boogie 2 (2008). \nhttps:\/\/github.com\/boogie-org\/boogie"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Lerch, J., Spth, J., Bodden, E., Mezini, M.: Access-path abstraction: scaling field-sensitive data-flow analysis with unbounded access paths (t). In: Automated Software Engineering (ASE), pp. 619\u2013629 (2015)","DOI":"10.1109\/ASE.2015.9"},{"issue":"1","key":"2_CR21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1391984.1391987","volume":"18","author":"O Lhot\u00e1k","year":"2008","unstructured":"Lhot\u00e1k, O., Hendren, L.: Evaluating the benefits of context-sensitive points-to analysis using a bdd-based implementation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 18(1), 3 (2008)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"2_CR22","unstructured":"Microsoft: Static driver verifier. \nhttp:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff552808(v=vs.85).aspx"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_7"},{"issue":"5","key":"2_CR24","doi-asserted-by":"crossref","first-page":"1467","DOI":"10.1145\/186025.186041","volume":"16","author":"G Ramalingam","year":"1994","unstructured":"Ramalingam, G.: The undecidability of aliasing. ACM Trans. Program. Lang. Syst. 16(5), 1467\u20131471 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR25","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis, pp. 189\u2013234. Prentice-Hall, Englewood Cliffs, NJ (1981). Chap. 7"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-36946-9_8","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"M Sridharan","year":"2013","unstructured":"Sridharan, M., Chandra, S., Dolby, J., Fink, S.J., Yahav, E.: Alias analysis for object-oriented programs. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 196\u2013232. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-36946-9_8"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Principles of Programming Languages (POPL), pp. 32\u201341. ACM, New York (1996)","DOI":"10.1145\/237721.237727"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.S.: An efficient inclusion-based points-to analysis for strictly-typed languages. In: Static Analysis Symposium, pp. 180\u2013195 (2002)","DOI":"10.1007\/3-540-45789-5_15"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Zheng, X., Rugina, R.: Demand-driven alias analysis for c. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 197\u2013208. ACM, New York (2008)","DOI":"10.1145\/1328438.1328464"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,3]],"date-time":"2017-10-03T03:49:17Z","timestamp":1507002557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}