{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T20:49:43Z","timestamp":1771274983056,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031442445","type":"print"},{"value":"9783031442452","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-44245-2_5","type":"book-chapter","created":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T15:02:30Z","timestamp":1698073350000},"page":"65-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Unconstrained Variable Oracles for\u00a0Faster Numeric Static Analyses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5150-0393","authenticated-orcid":false,"given":"Vincenzo","family":"Arceri","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2983-9251","authenticated-orcid":false,"given":"Greta","family":"Dolcetti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6388-2053","authenticated-orcid":false,"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,10,24]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-44716-4_20","volume-title":"Functional and Logic Programming","author":"G Amato","year":"2001","unstructured":"Amato, G., Spoto, F.: Abstract compilation for sharing analysis. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol. 2024, pp. 311\u2013325. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44716-4_20"},{"key":"5_CR2","doi-asserted-by":"publisher","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. 14\u201319. ACM (2023). https:\/\/doi.org\/10.1145\/3589250.3596141","DOI":"10.1145\/3589250.3596141"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Arceri, V., Mastroeni, I.: Analyzing dynamic code: a sound abstract interpreter for $$Evil$$ eval. ACM Trans. Priv. Secur. 24(2), 10:1\u201310:38 (2021). https:\/\/doi.org\/10.1145\/3426470","DOI":"10.1145\/3426470"},{"key":"5_CR4","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":"5_CR5","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":"Computer Aided Verification","author":"A Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: A direct encoding for NNC polyhedra. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 230\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_13"},{"key":"5_CR6","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":"Static Analysis","author":"A Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 146\u2013165. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_11"},{"key":"5_CR7","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":"5_CR8","doi-asserted-by":"publisher","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: Cytron, R., Gupta, R. (eds.) Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, 9\u201311 June 2003, pp. 196\u2013207. ACM (2003). https:\/\/doi.org\/10.1145\/781131.781153","DOI":"10.1145\/781131.781153"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-61053-7_62","volume-title":"Compiler Construction","author":"D Boucher","year":"1996","unstructured":"Boucher, D., Feeley, M.: Abstract compilation: a new implementation paradigm for static analysis. In: Gyim\u00f3thy, T. (ed.) CC 1996. LNCS, vol. 1060, pp. 192\u2013207. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61053-7_62"},{"key":"5_CR10","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":"Software Engineering and Formal Methods","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: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271\u2013277. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_20"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-32304-2_19","volume-title":"Static Analysis","author":"P Cousot","year":"2019","unstructured":"Cousot, P.: Abstract semantic dependency. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 389\u2013410. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_19"},{"key":"5_CR12","doi-asserted-by":"publisher","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. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Cousot, P., Giacobazzi, R., Ranzato, F.: A$${^2}$$I: abstract$${^2}$$ interpretation. Proc. ACM Program. Lang. 3(POPL), 42:1\u201342:31 (2019). https:\/\/doi.org\/10.1145\/3290355","DOI":"10.1145\/3290355"},{"key":"5_CR14","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"},{"issue":"6","key":"5_CR15","doi-asserted-by":"publisher","first-page":"974","DOI":"10.1017\/S1471068421000211","volume":"22","author":"E De Angelis","year":"2022","unstructured":"De Angelis, E., Fioravanti, F., Gallagher, J.P., Hermenegildo, M.V., Pettorossi, A., Proietti, M.: Analysis and transformation of constrained horn clauses for program verification. Theory Pract. Log. Program. 22(6), 974\u20131042 (2022). https:\/\/doi.org\/10.1017\/S1471068421000211","journal-title":"Theory Pract. Log. Program."},{"key":"5_CR16","doi-asserted-by":"publisher","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. 1\u20136. ACM (2021). https:\/\/doi.org\/10.1145\/3460946.3464316","DOI":"10.1145\/3460946.3464316"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/0743-1066(95)00038-0","volume":"25","author":"R Giacobazzi","year":"1995","unstructured":"Giacobazzi, R., Debray, S.K., Levi, G.: Generalized semantics and abstract interpretation for constraint logic programs. J. Log. Program. 25(3), 191\u2013247 (1995). https:\/\/doi.org\/10.1016\/0743-1066(95)00038-0","journal-title":"J. Log. Program."},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-030-95561-8_8","volume-title":"Software Verification","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.) NSV VSTTE 2021. LNPSE, vol. 13124, pp. 122\u2013144. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_8"},{"issue":"1","key":"5_CR19","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. Formal Methods Syst. Des. 29(1), 79\u201395 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0013-2","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. In: Jeannet, B. (ed.) Third Workshop on Tools for Automatic Program Analysis, TAPAS 2012. Electronic Notes in Theoretical Computer Science, Deauville, France, 14 September 2012, vol. 289, pp. 15\u201325. Elsevier (2012). https:\/\/doi.org\/10.1016\/j.entcs.2012.11.003","DOI":"10.1016\/j.entcs.2012.11.003"},{"issue":"4","key":"5_CR21","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/0743-1066(92)90053-6","volume":"13","author":"MV Hermenegildo","year":"1992","unstructured":"Hermenegildo, M.V., Warren, R.A., Debray, S.K.: Global flow analysis as a practical compilation tool. J. Log. Program. 13(4), 349\u2013366 (1992). https:\/\/doi.org\/10.1016\/0743-1066(92)90053-6","journal-title":"J. Log. Program."},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Hong, H.S., Lee, I., Sokolsky, O.: Abstract slicing: a new approach to program slicing based on abstract interpretation and model checking. In: 5th IEEE International Workshop on Source Code Analysis and Manipulation (SCAM 2005), Budapest, Hungary, 30 September\u20131 October 2005, pp. 25\u201334. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/SCAM.2005.2","DOI":"10.1109\/SCAM.2005.2"},{"key":"5_CR23","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":"Computer Aided Verification","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.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Li, Y., Tan, T., M\u00f8ller, A., Smaragdakis, Y.: A principled approach to selective context sensitivity for pointer analysis. ACM Trans. Program. Lang. Syst. 42(2), 10:1\u201310:40 (2020). https:\/\/doi.org\/10.1145\/3381915","DOI":"10.1145\/3381915"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Mastroeni, I., Zanardini, D.: Abstract program slicing: an abstract interpretation-based approach to program slicing. ACM Trans. Comput. Log. 18(1), 7:1\u20137:58 (2017). https:\/\/doi.org\/10.1145\/3029052","DOI":"10.1145\/3029052"},{"key":"5_CR26","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":"Static Analysis","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: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) SAS 2021. LNCS, vol. 12913, pp. 323\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_16"},{"key":"5_CR27","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. ISRL, vol. 238, pp. 19\u201342. Springer, Singapore (2023). https:\/\/doi.org\/10.1007\/978-981-19-9601-6_2"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Oh, H., Lee, W., Heo, K., Yang, H., Yi, K.: Selective X-sensitive analysis guided by impact pre-analysis. ACM Trans. Program. Lang. Syst. 38(2), 6:1\u20136:45 (2016). https:\/\/doi.org\/10.1145\/2821504","DOI":"10.1145\/2821504"},{"key":"5_CR29","doi-asserted-by":"publisher","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, 18\u201320 January 2017, pp. 46\u201359. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009885","DOI":"10.1145\/3009837.3009885"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Tan, T., Li, Y., Xue, J.: Efficient and precise points-to analysis: modeling the heap by merging equivalent automata. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18\u201323 June 2017, pp. 278\u2013291. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062360","DOI":"10.1145\/3062341.3062360"},{"key":"5_CR31","unstructured":"Warren, R.A., Hermenegildo, M.V., Debray, S.K.: On the practicality of global flow analysis of logic programs. In: Kowalski, R.A., Bowen, K.A. (eds.) Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, 15\u201319 August 1988, vol. 2, pp. 684\u2013699. MIT Press (1988)"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Wei, G., Chen, Y., Rompf, T.: Staged abstract interpreters: fast and modular whole-program analysis via meta-programming. Proc. ACM Program. Lang. 3(OOPSLA), 126:1\u2013126:32 (2019). https:\/\/doi.org\/10.1145\/3360552","DOI":"10.1145\/3360552"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-44245-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T08:14:11Z","timestamp":1707380051000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-44245-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031442445","9783031442452"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-44245-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"24 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/sas-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}