{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T17:07:49Z","timestamp":1744736869769,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T00:00:00Z","timestamp":1718323200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005713","name":"Technische Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005713","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The weakly relational domain of <jats:italic>Octagons<\/jats:italic> offers a decent compromise between precision and efficiency for numerical properties. Here, we are concerned with the construction of non-numerical relational domains. We provide a general construction of weakly relational domains, which we exemplify with an extension of constant propagation by disjunctions. Since for the resulting domain of 2-disjunctive formulas satisfiability is NP-complete, we provide a general construction for a further, more abstract, weakly relational domain where the abstract operations of restriction and least upper bound can be efficiently implemented. In the second step, we consider a relational domain that tracks conjunctions of inequalities between variables, and between variables and constants for arbitrary partial orders of values. Examples are sub(multi)sets, as well as prefix, substring or scattered substring orderings on strings. When the partial order is a lattice, we provide precise polynomial algorithms for satisfiability, restriction, and the best abstraction of disjunction. Complementary to the constructions for lattices, we find that, in general, satisfiability of conjunctions is NP-complete. We therefore again provide polynomial abstract versions of restriction, conjunction, and join. By using our generic constructions, these domains are extended to weakly relational domains that additionally track <jats:italic>disjunctions<\/jats:italic>. For all our domains, we indicate how abstract transformers for assignments and guards can be constructed.<\/jats:p>","DOI":"10.1007\/s10009-024-00755-0","type":"journal-article","created":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T08:02:12Z","timestamp":1718352132000},"page":"479-494","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Non-numerical weakly relational domains"],"prefix":"10.1007","volume":"26","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":"Sarah","family":"Tilscher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Schwarz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,14]]},"reference":[{"key":"755_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-030-31784-3_16","volume-title":"Automated Technology for Verification and Analysis \u2013 17th International Symposium, ATVA 2019, Proceedings","author":"P.A. Abdulla","year":"2019","unstructured":"Abdulla, P.A., Atig, M.F., Diep, B.P., Hol\u00edk, L., Janku, P.: Chain-free string constraints. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis \u2013 17th International Symposium, ATVA 2019, Proceedings, Taipei, Taiwan, October 28-31, 2019. LNCS, vol.\u00a011781, pp.\u00a0277\u2013293. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16"},{"key":"755_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2013.04.006","volume":"92","author":"E. Albert","year":"2014","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Rom\u00e1n-D\u00edez, G.: Conditional termination of loops over heap-allocated data. Sci. Comput. Program. 92, 2\u201324 (2014). https:\/\/doi.org\/10.1016\/j.scico.2013.04.006","journal-title":"Sci. Comput. Program."},{"key":"755_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-94583-1_2","volume-title":"Verification, Model Checking, and Abstract Interpretation \u2013 23rd International Conference, VMCAI 2022, Proceedings","author":"V. Arceri","year":"2022","unstructured":"Arceri, V., Olliaro, M., Cortesi, A., Ferrara, P.: Relational string abstract domains. In: Finkbeiner, B., Wies, T. (eds.) Verification, Model Checking, and Abstract Interpretation \u2013 23rd International Conference, VMCAI 2022, Proceedings, Philadelphia, PA, USA, January 16\u201318, 2022, LNCS, vol.\u00a013182, pp.\u00a020\u201342. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_2"},{"key":"755_CR4","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-540-78163-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: An improved tight closure algorithm for integer octagonal constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) Verification, Model Checking, and Abstract Interpretation, pp.\u00a08\u201321. Springer, Berlin (2008)"},{"issue":"3","key":"755_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-009-0073-1","volume":"35","author":"R. Bagnara","year":"2009","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Form. Methods Syst. Des. 35(3), 279\u2013323 (2009). https:\/\/doi.org\/10.1007\/s10703-009-0073-1","journal-title":"Form. Methods Syst. Des."},{"key":"755_CR6","series-title":"Proceedings","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1109\/ISMVL.2000.848640","volume-title":"30th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2000","author":"B. Beckert","year":"2000","unstructured":"Beckert, B., H\u00e4hnle, R., Many\u00e0, F.: The 2-sat problem of regular signed CNF formulas. In: 30th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2000, Portland, Oregon, USA, May 23\u201325, 2000. Proceedings, pp.\u00a0331\u2013336. IEEE Comput. Soc., Los Alamitos (2000). https:\/\/doi.org\/10.1109\/ISMVL.2000.848640"},{"issue":"2","key":"755_CR7","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/s10703-017-0314-7","volume":"54","author":"A. Chawdhary","year":"2019","unstructured":"Chawdhary, A., Robbins, E., King, A.: Incrementally closing octagons. Form. Methods Syst. Des. 54(2), 232\u2013277 (2019). https:\/\/doi.org\/10.1007\/s10703-017-0314-7","journal-title":"Form. Methods Syst. Des."},{"issue":"POPL","key":"755_CR8","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/3158091","volume":"2","author":"T. Chen","year":"2018","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the ReplaceAll function. Proc. ACM Program. Lang. 2(POPL), 3:1\u20133:29 (2018). https:\/\/doi.org\/10.1145\/3158091","journal-title":"Proc. ACM Program. Lang."},{"key":"755_CR9","volume-title":"Principles of Abstract Interpretation","author":"P. Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"755_CR10","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Conference Record of the Fourth ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp.\u00a0238\u2013252. ACM, New York (1977). https:\/\/doi.org\/10.1145\/512950.512973."},{"issue":"4","key":"755_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/LOGCOM\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511\u2013547 (1992). https:\/\/doi.org\/10.1093\/LOGCOM\/2.4.511","journal-title":"J. Log. Comput."},{"key":"755_CR12","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/512760.512770","volume-title":"Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1978","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.\u00a084\u201396. ACM, New York (1978). https:\/\/doi.org\/10.1145\/512760.512770"},{"issue":"POPL","key":"755_CR13","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1145\/3571203","volume":"7","author":"J.D. Day","year":"2023","unstructured":"Day, J.D., Ganesh, V., Grewal, N., Manea, F.: On the expressive power of string constraints. Proc. ACM Program. Lang. 7(POPL), 278\u2013308 (2023). https:\/\/doi.org\/10.1145\/3571203","journal-title":"Proc. ACM Program. Lang."},{"key":"755_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-47764-0_12","volume-title":"Static Analysis, 8th International Symposium, SAS 2001, Proceedings","author":"N. Dor","year":"2001","unstructured":"Dor, N., Rodeh, M., Sagiv, S.: Cleanness checking of string manipulations in C programs via integer analysis. In: Cousot, P. (ed.) Static Analysis, 8th International Symposium, SAS 2001, Proceedings. Paris, France, July 16\u201318, 2001, LNCS, vol.\u00a02126, pp.\u00a0194\u2013212. Springer, Berlin (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0_12"},{"key":"755_CR15","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: What is decidable about strings? (2011)"},{"key":"755_CR16","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 Inform. 6, 133\u2013151 (1976). https:\/\/doi.org\/10.1007\/BF00268497","journal-title":"Acta Inform."},{"key":"755_CR17","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1109\/WCRE.2001.957836","volume-title":"WCRE\u2019 01","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE\u2019 01, p.\u00a0310. IEEE Comput. Soc., Los Alamitos (2001). https:\/\/doi.org\/10.1109\/WCRE.2001.957836"},{"key":"755_CR18","unstructured":"Min\u00e9, A.: Weakly relational numerical abstract domains. (Domaines num\u00e9riques abstraits faiblement relationnels). PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (2004). https:\/\/tel.archives-ouvertes.fr\/tel-00136630"},{"issue":"1","key":"755_CR19","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31\u2013100 (2006). https:\/\/doi.org\/10.1007\/s10990-006-8609-1","journal-title":"High.-Order Symb. Comput."},{"key":"755_CR20","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/964001.964029","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004","author":"M. M\u00fcller-Olm","year":"2004","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, January 14\u201316, 2004, pp.\u00a0330\u2013341. ACM, New York (2004). https:\/\/doi.org\/10.1145\/964001.964029"},{"issue":"5","key":"755_CR21","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/1275497.1275504","volume":"29","author":"M. M\u00fcller-Olm","year":"2007","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst. 29(5), 29 (2007). https:\/\/doi.org\/10.1145\/1275497.1275504","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"755_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol.\u00a03385, pp.\u00a025\u201341. Springer, Berlin (2005)"},{"key":"755_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-031-44245-2_21","volume-title":"Static Analysis \u2013 30th International Symposium, SAS 2023, Proceedings","author":"M. Schwarz","year":"2023","unstructured":"Schwarz, M., Seidl, H.: Octagons revisited - elegant proofs and simplified algorithms. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis \u2013 30th International Symposium, SAS 2023, Proceedings, Cascais, Portugal, October 22\u201324, 2023. LNCS, vol.\u00a014284, pp.\u00a0485\u2013507. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_21"},{"key":"755_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-031-30044-8_2","volume-title":"Programming Languages and Systems \u2013 32nd European Symposium on Programming, ESOP 2023, ETAPS 2023, Proceedings","author":"M. Schwarz","year":"2023","unstructured":"Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: Wies, T. (ed.) Programming Languages and Systems \u2013 32nd European Symposium on Programming, ESOP 2023, ETAPS 2023, Proceedings, Paris, France, April 22\u201327, 2023, LNCS, vol.\u00a013990, pp.\u00a028\u201358. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_2"},{"key":"755_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/3-540-45013-0_7","volume-title":"Logic Based Program Synthesis and Transformation, 12th International Workshop, LOPSTR 2002, Revised Selected Papers","author":"A. Simon","year":"2002","unstructured":"Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) Logic Based Program Synthesis and Transformation, 12th International Workshop, LOPSTR 2002, Revised Selected Papers, Madrid, Spain, September 17-20, 2002. LNCS, vol.\u00a02664, pp.\u00a071\u201389. Springer, Berlin (2002). https:\/\/doi.org\/10.1007\/3-540-45013-0_7"},{"key":"755_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-22306-8_3","volume-title":"Model Checking Software \u2013 18th International SPIN Workshop, Proceedings","author":"F. Yu","year":"2011","unstructured":"Yu, F., Bultan, T., Hardekopf, B.: String abstractions for string verification. In: Groce, A., Musuvathi, M. (eds.) Model Checking Software \u2013 18th International SPIN Workshop, Proceedings, Snowbird, UT, USA, July 14\u201315, 2011. LNCS, vol.\u00a06823, pp.\u00a020\u201337. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22306-8_3"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00755-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00755-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00755-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:03:15Z","timestamp":1725530595000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00755-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,14]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,8]]}},"alternative-id":["755"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00755-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2024,6,14]]},"assertion":[{"value":"4 June 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}