{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:40:03Z","timestamp":1745944803721,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031562211"},{"type":"electronic","value":"9783031562228"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-56222-8_16","type":"book-chapter","created":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T08:02:30Z","timestamp":1710835350000},"page":"281-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["2-Pointer Logic"],"prefix":"10.1007","author":[{"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"Erhard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Schwarz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarah","family":"Tilscher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-94583-1_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Arceri","year":"2022","unstructured":"Arceri, V., Olliaro, M., Cortesi, A., Ferrara, P.: Relational string abstract domains. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 20\u201342. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_2"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Chang, B.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Banerjee, A., Danvy, O., Doh, K., Hatcliff, J. (eds.) Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19\u201320th September 2013, EPTCS, vol. 129, pp. 161\u2013185 (2013). https:\/\/doi.org\/10.4204\/EPTCS.129.11","DOI":"10.4204\/EPTCS.129.11"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84\u201396. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-031-44245-2_15","volume-title":"Static Analysis","author":"J Giet","year":"2023","unstructured":"Giet, J., Ridoux, F., Rival, X.: A product of shape and sequence abstractions. In: Hermenegildo, M.V., Morales, J.F. (eds.) SAS 2023. LNCS, vol. 14284, pp. 310\u2013342. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_15"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI 2007, pp. 266\u2013277. ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250765","DOI":"10.1145\/1250734.1250765"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-30538-5_26","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"S Gulwani","year":"2004","unstructured":"Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of uninterpreted functions. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 311\u2013323. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_26"},{"issue":"3","key":"16_CR7","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/S10703-021-00366-4","volume":"57","author":"H Illous","year":"2021","unstructured":"Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. Formal Methods Syst. Des. 57(3), 343\u2013400 (2021). https:\/\/doi.org\/10.1007\/S10703-021-00366-4","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-031-30823-9_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Korovin","year":"2023","unstructured":"Korovin, K., Kov\u00e1cs, L., Reger, G., Schoisswohl, J., Voronkov, A.: ALASCA: reasoning in quantified linear arithmetic. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 647\u2013665. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_33"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74105-3. ISBN 978-3-540-74104-6","DOI":"10.1007\/978-3-540-74105-3"},{"key":"16_CR10","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 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44978-7_10"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE 2001, p. 310. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/WCRE.2001.957836","DOI":"10.1109\/WCRE.2001.957836"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Irwin, M.J., Bosschere, K.D. (eds.) Proceedings of the 2006 ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Ontario, Canada, 14\u201316 June 2006, pp. 54\u201363. ACM (2006). https:\/\/doi.org\/10.1145\/1134650.1134659","DOI":"10.1145\/1134650.1134659"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symbol. Comput. 19(1), 31\u2013100 (2006). https:\/\/doi.org\/10.1007\/s10990-006-8609-1. ISSN 1388-3690","DOI":"10.1007\/s10990-006-8609-1"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1016","DOI":"10.1007\/978-3-540-27836-8_85","volume-title":"Automata, Languages and Programming","author":"M M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: A note on Karr\u2019s algorithm. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016\u20131028. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_85"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, 14\u201316 January 2004, pp. 330\u2013341. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964029","DOI":"10.1145\/964001.964029"},{"key":"16_CR16","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. 4960, pp. 178\u2013192. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78739-6_15"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979). https:\/\/doi.org\/10.1145\/357073.357079. ISSN 0164-0925","DOI":"10.1145\/357073.357079"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980). https:\/\/doi.org\/10.1145\/322186.322198. ISSN 0004-5411","DOI":"10.1145\/322186.322198"},{"issue":"1","key":"16_CR19","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theoret. Comput. Sci. 375(1), 271\u2013307 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.035","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"16_CR20","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3211968","volume":"62","author":"PW O\u2019Hearn","year":"2019","unstructured":"O\u2019Hearn, P.W.: Separation logic. Commun. ACM 62(2), 86\u201395 (2019). https:\/\/doi.org\/10.1145\/3211968","journal-title":"Commun. ACM"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Sagiv, M., Wilhelm, R.: Shape analysis and applications. In: Srikant, Y.N., Shankar, P. (eds.) The Compiler Design Handbook: Optimizations and Machine Code Generation, 2nd edn, p. 12. CRC Press (2007)","DOI":"10.1201\/9781420043839.ch12"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, 16\u201319 June 2001, pp. 19\u201328. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932479","DOI":"10.1109\/LICS.2001.932479"},{"issue":"3","key":"16_CR23","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"S Sagiv","year":"2002","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002). https:\/\/doi.org\/10.1145\/514188.514190","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Seidl, H., Erhard, J., Tilscher, S., Schwarz, M.: Non-numerical weakly relational domains (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.05165","DOI":"10.48550\/ARXIV.2401.05165"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1007\/978-3-642-05089-3_41","volume-title":"FM 2009: Formal Methods","author":"H Seidl","year":"2009","unstructured":"Seidl, H., Vojdani, V., Vene, V.: A smooth combination of linear and Herbrand equalities for polynomial time must-alias analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 644\u2013659. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_41"},{"issue":"1","key":"16_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984). https:\/\/doi.org\/10.1145\/2422.322411","journal-title":"J. ACM"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, New York, NY, USA, pp. 46\u201359. Association for Computing Machinery (2017). https:\/\/doi.org\/10.1145\/3009837.3009885. ISBN 9781450346603","DOI":"10.1145\/3009837.3009885"}],"container-title":["Lecture Notes in Computer Science","Taming the Infinities of Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-56222-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T22:03:27Z","timestamp":1730930607000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-56222-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031562211","9783031562228"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-56222-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"20 March 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}