{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:40Z","timestamp":1740107980708,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T00:00:00Z","timestamp":1724716800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T00:00:00Z","timestamp":1724716800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004770","name":"Universit\u00e0 degli Studi di Parma","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004770","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,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In the context of abstract interpretation-based static analysis, we propose a new abstract operator modeling the <jats:italic>split<\/jats:italic> of control flow paths: the goal of the operator is to enable a more efficient analysis when using abstract domains that are computationally expensive, having no negative effect on precision, and occasionally resulting in a more precise analysis. We focus on the case of conditional branches guarded by numeric linear constraints, including implicit numerical branches. We provide an experimental evaluation of real-world test cases, showing that by using the split operator we can achieve significant efficiency improvements with respect to the classical approach for a static analysis based on the domain of convex polyhedra. We also briefly discuss the applicability of this new operator to different, possibly non-numeric abstract domains.<\/jats:p>","DOI":"10.1007\/s10009-024-00761-2","type":"journal-article","created":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T09:03:04Z","timestamp":1724749384000},"page":"573-588","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Speeding up static analysis with the split operator"],"prefix":"10.1007","volume":"26","author":[{"given":"Vincenzo","family":"Arceri","sequence":"first","affiliation":[]},{"given":"Greta","family":"Dolcetti","sequence":"additional","affiliation":[]},{"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,27]]},"reference":[{"key":"761_CR1","doi-asserted-by":"publisher","DOI":"10.3390\/app10103525","volume":"10","author":"V. Arceri","year":"2020","unstructured":"Arceri, V., Mastroeni, I., Xu, S.: Static analysis for ecmascript string manipulation programs. Appl. Sci. 10, 3525 (2020). https:\/\/doi.org\/10.3390\/app10103525","journal-title":"Appl. Sci."},{"key":"761_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-031-21037-2_2","volume-title":"Proceedings","author":"V. Arceri","year":"2022","unstructured":"Arceri, V., Mastroeni, I., Zaffanella, E.: Decoupling the ascending and descending phases in abstract interpretation. In: Sergey, I. (ed.) Proceedings, Programming Languages and Systems\u00a0- 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022. Lecture Notes in Computer Science, vol.\u00a013658, pp.\u00a025\u201344. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-21037-2_2"},{"key":"761_CR3","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/3589250.3596141","volume-title":"Proceedings of the 12th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis","author":"V. Arceri","year":"2023","unstructured":"Arceri, V., Dolcetti, G., Zaffanella, E.: Speeding up static analysis with the split operator. In: Ferrara, P., Hadarean, L. (eds.) Proceedings of the 12th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2023, Orlando, FL, USA, 17 June 2023, pp.\u00a014\u201319. ACM (2023). https:\/\/doi.org\/10.1145\/3589250.3596141"},{"key":"761_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-71410-1_16","volume-title":"Revised Selected Papers","author":"R. Bagnara","year":"2006","unstructured":"Bagnara, R., Dobson, K.L., Hill, P.M., Mundell, M., Zaffanella, E.: Grids: a domain for analyzing the distribution of numerical values. In: Puebla, G. (ed.) Revised Selected Papers, Logic-Based Program Synthesis and Transformation, 16th International Symposium, LOPSTR 2006, Venice, Italy, July 12\u201314, 2006. Lecture Notes in Computer Science, vol.\u00a04407, pp.\u00a0219\u2013235. Springer (2006). https:\/\/doi.org\/10.1007\/978-3-540-71410-1_16"},{"issue":"3\u20134","key":"761_CR5","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/s10009-007-0029-y","volume":"9","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Int. J. Softw. Tools Technol. Transf. 9(3\u20134), 413\u2013414 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0029-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1\u20132","key":"761_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008). https:\/\/doi.org\/10.1016\/j.scico.2007.08.001","journal-title":"Sci. Comput. Program."},{"key":"761_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-319-96145-3_13","volume-title":"Proceedings, Part I","author":"A. Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: A direct encoding for NNC polyhedra. In: Chockler, H., Weissenbacher, G. (eds.) Proceedings, Part I, Computer Aided Verification\u00a0- 30th International Conference, CAV 2018, Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018. Lecture Notes in Computer Science, vol.\u00a010981, pp.\u00a0230\u2013248. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_13"},{"key":"761_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-99725-4_11","volume-title":"Proceedings","author":"A. Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed.) Proceedings, Static Analysis\u00a0- 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018. Lecture Notes in Computer Science, vol.\u00a011002, pp.\u00a0146\u2013165. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_11"},{"key":"761_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-030-32304-2_10","volume-title":"Proceedings","author":"A. Becchi","year":"2019","unstructured":"Becchi, A., Zaffanella, E.: Revisiting polyhedral analysis for hybrid systems. In: Chang, B.E. (ed.) Proceedings, Static Analysis\u00a0- 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019. Lecture Notes in Computer Science, vol.\u00a011822, pp.\u00a0183\u2013202. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_10"},{"key":"761_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104620","volume":"275","author":"A. Becchi","year":"2020","unstructured":"Becchi, A., Zaffanella, E.: PPLite: zero-overhead encoding of NNC polyhedra. Inf. Comput. 275, 104620 (2020) https:\/\/doi.org\/10.1016\/j.ic.2020.104620","journal-title":"Inf. Comput."},{"key":"761_CR11","volume-title":"Lattice Theory, Colloquium Publications","author":"G. Birkhoff","year":"1967","unstructured":"Birkhoff, G.: Lattice Theory, Colloquium Publications, vol.\u00a0XXV, 3rd edn. Am. Math. Soc., Providence (1967)","edition":"3"},{"key":"761_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-10431-7_20","volume-title":"Proceedings","author":"G. Brat","year":"2014","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Proceedings, Software Engineering and Formal Methods\u00a0- 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Lecture Notes in Computer Science, vol.\u00a08702, pp.\u00a0271\u2013277. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_20"},{"issue":"6","key":"761_CR13","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","volume":"8","author":"N.V. Chernikova","year":"1968","unstructured":"Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. USSR Comput. Math. Math. Phys. 8(6), 282\u2013293 (1968)","journal-title":"USSR Comput. Math. Math. Phys."},{"key":"761_CR14","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, Los Angeles, California, USA, January 1977","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 (1977). https:\/\/doi.org\/10.1145\/512950.512973."},{"key":"761_CR15","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, Tucson, Arizona, USA, January 1978","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 Press (1978). https:\/\/doi.org\/10.1145\/512760.512770"},{"key":"761_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3460946.3464316","volume-title":"SOAP@PLDI 2021: Proceedings of the 10th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, Virtual Event, Canada, 22 June, 2021","author":"P. Ferrara","year":"2021","unstructured":"Ferrara, P., Negrini, L., Arceri, V., Cortesi, A.: Static analysis for dummies: experiencing lisa. In: Do, L.N.Q., Urban, C. (eds.) SOAP@PLDI 2021: Proceedings of the 10th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, Virtual Event, Canada, 22 June, 2021, pp.\u00a01\u20136. ACM (2021). https:\/\/doi.org\/10.1145\/3460946.3464316"},{"issue":"3","key":"761_CR17","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G. Frehse","year":"2008","unstructured":"Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0062-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"761_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-030-88806-0_7","volume-title":"Proceedings","author":"G. Gange","year":"2021","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Disjunctive interval analysis. In: Dragoi, C., Mukherjee, S., Namjoshi, K.S. (eds.) Proceedings, Static Analysis\u00a0- 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021. Lecture Notes in Computer Science, vol.\u00a012913, pp.\u00a0144\u2013165. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_7"},{"key":"761_CR19","unstructured":"Genov, B.: The convex hull problem in practice: Improving the running time of the double description method. PhD thesis, University of Bremen, Germany (2014)"},{"key":"761_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-15769-1_18","volume-title":"Proceedings","author":"A. Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Boxes: a symbolic abstract domain of boxes. In: Cousot, R., Martel, M. (eds.) Proceedings, Static Analysis\u00a0- 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Lecture Notes in Computer Science, vol.\u00a06337, pp.\u00a0287\u2013303. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_18"},{"key":"761_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-030-95561-8_8","volume-title":"Software Verification\u00a0- 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers","author":"A. Gurfinkel","year":"2021","unstructured":"Gurfinkel, A., Navas, J.A.: Abstract interpretation of LLVM with a region-based memory model. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification\u00a0- 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a013124, pp.\u00a0122\u2013144. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_8."},{"key":"761_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Proceedings, Part I","author":"A. Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) Proceedings, Part I, Computer Aided Verification\u00a0- 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015. Lecture Notes in Computer Science, vol.\u00a09206, pp.\u00a0343\u2013361. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"issue":"1","key":"761_CR23","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10703-006-0013-2","volume":"29","author":"N. Halbwachs","year":"2006","unstructured":"Halbwachs, N., Merchat, D., Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations. Form. Methods Syst. Des. 29(1), 79\u201395 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0013-2","journal-title":"Form. Methods Syst. Des."},{"key":"761_CR24","series-title":"Electronic Notes in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.entcs.2012.11.003","volume-title":"Third Workshop on Tools for Automatic Program Analysis","author":"J. Henry","year":"2012","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. In: Third Workshop on Tools for Automatic Program Analysis, TAPAS 2012, Deauville, France, September 14, 2012. Electronic Notes in Theoretical Computer Science, vol.\u00a0289, pp.\u00a015\u201325. Elsevier (2012). https:\/\/doi.org\/10.1016\/j.entcs.2012.11.003"},{"key":"761_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Proceedings","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) Proceedings, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26\u00a0- July 2, 2009. Lecture Notes in Computer Science, vol.\u00a05643, pp.\u00a0661\u2013667. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"761_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-030-65474-0_3","volume-title":"Proceedings","author":"S.K. Kim","year":"2020","unstructured":"Kim, S.K., Venet, A.J., Thakur, A.V.: Memory-efficient fixpoint computation. In: Pichardie, D., Sighireanu, M. (eds.) Proceedings, Static Analysis\u00a0- 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020. Lecture Notes in Computer Science, vol.\u00a012389, pp.\u00a035\u201364. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-65474-0_3"},{"key":"761_CR27","unstructured":"Le Verge, H.: A note on Chernikova\u2019s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France (1992)"},{"key":"761_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-030-88806-0_16","volume-title":"Proceedings","author":"R. Monat","year":"2021","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: A multilanguage static analysis of python programs with native C extensions. In: Dragoi, C., Mukherjee, S., Namjoshi, K.S. (eds.) Proceedings, Static Analysis\u00a0- 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17\u201319, 2021. Lecture Notes in Computer Science, vol.\u00a012913, pp.\u00a0323\u2013345. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_16"},{"key":"761_CR29","series-title":"Annals of Mathematics Studies","first-page":"51","volume-title":"Contributions to the Theory of Games\u00a0\u2013 Volume II","author":"T.S. Motzkin","year":"1953","unstructured":"Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Kuhn, H.W., Tucker, A.W. (eds.) Contributions to the Theory of Games\u00a0\u2013 Volume II, Annals of Mathematics Studies, vol.\u00a028, pp.\u00a051\u201373. Princeton University Press, Princeton (1953)"},{"key":"761_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-030-67067-2_13","volume-title":"Proceedings","author":"L. Negrini","year":"2021","unstructured":"Negrini, L., Arceri, V., Ferrara, P., Cortesi, A.: Twinning automata and regular expressions for string static analysis. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Proceedings, Verification, Model Checking, and Abstract Interpretation\u00a0- 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021. Lecture Notes in Computer Science, vol.\u00a012597, pp.\u00a0267\u2013290. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_13"},{"key":"761_CR31","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-981-19-9601-6_2","volume-title":"Challenges of Software Verification","author":"L. Negrini","year":"2023","unstructured":"Negrini, L., Ferrara, P., Arceri, V., Cortesi, A.: Lisa: a generic framework for multilanguage static analysis. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds.) Challenges of Software Verification, pp.\u00a019\u201342. Springer Nature Singapore, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-19-9601-6_2"},{"key":"761_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-35873-9_26","volume-title":"Proceedings","author":"M. Pelleau","year":"2013","unstructured":"Pelleau, M., Min\u00e9, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Proceedings, Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22. Lecture Notes in Computer Science, vol.\u00a07737, pp.\u00a0434\u2013454. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_26"},{"key":"761_CR33","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/3009837.3009885","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages","author":"G. Singh","year":"2017","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pp.\u00a046\u201359. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009885"},{"key":"761_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-030-54997-8_8","volume-title":"Revised Selected Papers, Part II","author":"G. Ziat","year":"2019","unstructured":"Ziat, G., Mar\u00e9chal, A., Pelleau, M., Min\u00e9, A., Truchet, C.: Combination of boxes and polyhedra abstractions for constraint solving. In: Sekerinski, E., Moreira, N., Oliveira, J.N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J.C., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P., Delmas, D. (eds.) Revised Selected Papers, Part II, Formal Methods. FM 2019 International Workshops, Porto, Portugal, October 7-11, 2019. Lecture Notes in Computer Science, vol.\u00a012233, pp.\u00a0119\u2013135. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-54997-8_8"}],"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-00761-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00761-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00761-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,27]],"date-time":"2024-09-27T13:05:37Z","timestamp":1727442337000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00761-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,27]]},"references-count":34,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["761"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00761-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2024,8,27]]},"assertion":[{"value":"14 August 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 August 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}