{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:32:59Z","timestamp":1745944379556},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_41","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"644-659","source":"Crossref","is-referenced-by-count":5,"title":["A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis"],"prefix":"10.1007","author":[{"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Varmo","family":"Vene","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"41_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-45657-0_35","volume-title":"Computer Aided Verification","author":"A. Chakrabarti","year":"2002","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T., Jurdzi\u0144ski, M., Mang, F.: Interface compatibility checking for software modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 428\u2013663. Springer, Heidelberg (2002)"},{"key":"41_CR2","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1145\/178243.178263","volume-title":"PLDI 1994","author":"A. Deutsch","year":"1994","unstructured":"Deutsch, A.: Interprocedural may-alias analysis for pointers: beyond k-limiting. In: PLDI 1994, pp. 230\u2013241. ACM Press, New York (1994)"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-540-27864-1_17","volume-title":"Static Analysis","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 212\u2013227. Springer, Heidelberg (2004)"},{"key":"41_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11693024_19","volume-title":"Programming Languages and Systems","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 279\u2013293. Springer, Heidelberg (2006)"},{"key":"41_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-540-73368-3_42","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: An abstract domain for analyzing heap-manipulating low-level software. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 379\u2013392. Springer, Heidelberg (2007)"},{"key":"41_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-71316-6_18","volume-title":"Programming Languages and Systems","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 253\u2013267. Springer, Heidelberg (2007)"},{"issue":"4","key":"41_CR7","doi-asserted-by":"publisher","first-page":"848","DOI":"10.1145\/325478.325519","volume":"21","author":"M. Hind","year":"1999","unstructured":"Hind, M., Burke, M., Carini, P., Choi, J.-D.: Interprocedural pointer alias analysis. ACM Trans. Prog. Lang. Syst.\u00a021(4), 848\u2013894 (1999)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"issue":"6","key":"41_CR8","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1109\/MC.2006.212","volume":"39","author":"G.J. Holzmann","year":"2006","unstructured":"Holzmann, G.J.: The power of ten: Rules for developing safety critical code. IEEE Computer\u00a039(6), 95\u201397 (2006)","journal-title":"IEEE Computer"},{"issue":"2","key":"41_CR9","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06(2), 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"41_CR10","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1145\/512927.512945","volume-title":"POPL 1973","author":"G.A. Kildall","year":"1973","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194\u2013206. ACM Press, New York (1973)"},{"key":"41_CR11","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/1294261.1294272","volume-title":"SOSP 2007","author":"S. Lu","year":"2007","unstructured":"Lu, S., Park, S., Hu, C., Ma, X., Jiang, W., Li, Z., Popa, R.A., Zhou, Y.: MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In: SOSP 2007, pp. 103\u2013116. ACM Press, New York (2007)"},{"key":"41_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/978-3-540-30579-8_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. M\u00fcller-Olm","year":"2005","unstructured":"M\u00fcller-Olm, M., R\u00fcthing, O., Seidl, H.: Checking Herbrand equalities and beyond. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 79\u201396. Springer, Heidelberg (2005)"},{"key":"41_CR13","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/964001.964029","volume-title":"POPL 2004","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL 2004, pp. 330\u2013341. ACM Press, New York (2004)"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Prog. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275504"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-78739-6_15","volume-title":"Programming Languages and Systems","author":"M. M\u00fcller-Olm","year":"2008","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Upper adjoints for fast inter-procedural variable equalities. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 178\u2013192. Springer, Heidelberg (2008)"},{"key":"41_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-540-31987-0_4","volume-title":"Programming Languages and Systems","author":"M. M\u00fcller-Olm","year":"2005","unstructured":"M\u00fcller-Olm, M., Seidl, H., Steffen, B.: Interprocedural Herbrand equalities. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 31\u201345. Springer, Heidelberg (2005)"},{"key":"41_CR17","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/1190216.1190265","volume-title":"POPL 2007","author":"M. Naik","year":"2007","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: POPL 2007, pp. 327\u2013338. ACM Press, New York (2007)"},{"issue":"2","key":"41_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Prog. Lang. Syst.\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"41_CR19","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/800113.803646","volume-title":"STOC 1976","author":"M. Paterson","year":"1976","unstructured":"Paterson, M., Wegman, M.N.: Linear unification. In: STOC 1976, pp. 181\u2013186. ACM Press, New York (1976)"},{"key":"41_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/11823230_7","volume-title":"Static Analysis","author":"P. Pratikakis","year":"2006","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: Existential label flow inference via CFL reachability. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 88\u2013106. Springer, Heidelberg (2006)"},{"key":"41_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-03237-0_13","volume-title":"SAS 2009","author":"H. Seidl","year":"2009","unstructured":"Seidl, H., Vojdani, V.: Region analysis for race detection. In: SAS 2009. LNCS, vol.\u00a05673, pp. 171\u2013187. Springer, Heidelberg (2009)"},{"key":"41_CR22","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"ESOP \u201990","author":"B. Steffen","year":"1990","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: The value flow graph: A program representation for optimal program transformations. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol.\u00a0432, pp. 232\u2013247. Springer, Heidelberg (1990)"},{"key":"41_CR23","first-page":"141","volume":"30","author":"V. Vojdani","year":"2009","unstructured":"Vojdani, V., Vene, V.: Goblint: Path-sensitive data race analysis. Annales Univ. Sci. Budapest., Sect. Comp.\u00a030, 141\u2013155 (2009)","journal-title":"Annales Univ. Sci. Budapest., Sect. Comp."}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:39Z","timestamp":1606186059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}