Skip to main content
Springer Nature Link
Log in

Relating Distances and Abstractions

An Abstract Interpretation Perspective

  • Conference paper
  • First Online:
Image Static Analysis (SAS 2025)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 16100))

Included in the following conference series:

  • 317 Accesses

  • 2 Citations

Abstract

We establish a formal relation between quantitative and semantic approximations—formalized by pre-metrics and upper closure operators (ucos), respectively—by means of Galois connections. This connection reveals that it is far from trivial for a pre-metric to uniquely identify a uco, highlighting the structural constraints and, more generally, the distinct identity inherent to semantic approximations.

Building on this foundation, we introduce a general composition of semantic and quantitative approximations. This allows us to define a new confidentiality property, called Partial Abstract Non-Interference, that measures bounded variations in program behavior over abstract properties of data. We then relate this property to Partial Completeness in abstract interpretation, revealing a deeper connection between static analysis precision and security guarantees.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+
from $39.99 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

Notes

  1. 1.

    For the sake of readability, in the following, we represent sets of numbers by the sequences of their elements without separators, e.g., \(\{1,2\}\) is represented by 12.

  2. 2.

    This definition of Completeness is also called Backward-Completeness [26].

References

  1. Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: A logic for locally complete abstract interpretations. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470608

  2. Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: Abstract interpretation repair. In: Jhala, R., Dillig, I. (eds.) PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 426–441. ACM (2022). https://doi.org/10.1145/3519939.3523453

  3. Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: A correctness and incorrectness program logic. J. ACM 70(2), 15:1–15:45 (2023). https://doi.org/10.1145/3582267

  4. Campion, M., Dalla Preda, M., Giacobazzi, R.: Abstract interpretation of indexed grammars. In: Chang, B.E. (ed.) 26th Static Analysis Symposium (SAS 2019). Lecture Notes in Computer Science, vol. 11822, pp. 121–139. Springer (2019). https://doi.org/10.1007/978-3-030-32304-2_7

  5. Campion, M., Dalla Preda, M., Giacobazzi, R.: Partial (in)completeness in abstract interpretation: limiting the imprecision in program analysis. Proc. ACM Program. Lang. 6(POPL), 1–31 (2022). https://doi.org/10.1145/3498721

  6. Campion, M., Dalla Preda, M., Giacobazzi, R., Urban, C.: Monotonicity and the precision of program analysis. Proc. ACM Program. Lang. 8(POPL), 1629–1662 (2024). https://doi.org/10.1145/3632897

  7. Campion, M., Preda, M.D., Giacobazzi, R.: On the properties of partial completeness in abstract interpretation. In: Lago, U.D., Gorla, D. (eds.) Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022. CEUR Workshop Proceedings, vol. 3284, pp. 79–85. CEUR-WS.org (2022). https://ceur-ws.org/Vol-3284/8665.pdf

  8. Campion, M., Urban, C., Preda, M.D., Giacobazzi, R.: A formal framework to measure the incompleteness of abstract interpretations. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis - 30th International Symposium, SAS 2023. Lecture Notes in Computer Science, vol. 14284, pp. 114–138. Springer (2023). https://doi.org/10.1007/978-3-031-44245-2_7

  9. Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 57–70. POPL ’10, Association for Computing Machinery (2010). https://doi.org/10.1145/1706299.1706308

  10. Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs 55(8), 107–115 (2012). https://doi.org/10.1145/2240236.2240262

  11. Chaudhuri, S., Gulwani, S., Lublinerman, R., NavidPour, S.: Proving programs robust. In: Gyimóthy, T., Zeller, A. (eds.) SIGSOFT/FSE’11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19), pp. 102–112. ACM (2011). https://doi.org/10.1145/2025113.2025131

  12. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010). https://doi.org/10.3233/JCS-2009-0393

    Article  Google Scholar 

  13. Cousot, P.: Principles of Abstract Interpretation. The MIT Press, Cambridge, Mass (2021)

    MATH  Google Scholar 

  14. 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–252. ACM (1977). https://doi.org/10.1145/512950.512973

  15. Cousot, P., Cousot, R.: A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice. Portugaliae Mathematica 38(1-2), 185–198 (1979). http://eudml.org/doc/115380

  16. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, pp. 269–282. ACM Press (1979). https://doi.org/10.1145/567752.567778

  17. Geometry of Cuts and Metrics. AC, vol. 15. Springer, Heidelberg (1997). https://doi.org/10.1007/978-3-642-04295-9

  18. Di Pierro, A., Hankin, C., Wiklicky, H.: Approximate non-interference. J. Comput. Secur. 12(1), 37–82 (2004). https://doi.org/10.3233/JCS-2004-12103

    Article  Google Scholar 

  19. Di Pierro, A., Wiklicky, H.: Measuring the precision of abstract interpretations. In: Lau, K. (ed.) 10th Logic Based Program Synthesis and Transformation (LOPSTR’00). LNCS, vol. 2042, pp. 147–164. Springer (2000)

    Google Scholar 

  20. Dwork, C., McSherry, F., Nissim, K., Smith, A.D.: Calibrating noise to sensitivity in private data analysis. In: Halevi, S., Rabin, T. (eds.) Theory of Cryptography, Third Theory of Cryptography Conference, TCC 2006. LNCS, vol. 3876, pp. 265–284. Springer (2006). https://doi.org/10.1007/11681878_14

  21. Giacobazzi, R., Mastroeni, I.: Proving abstract non-interference. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 280–294. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30124-0_23

    Chapter  Google Scholar 

  22. Giacobazzi, R., Mastroeni, I.: Adjoining classified and unclassified information by abstract interpretation. J. Comput. Secur. 18(5), 751–797 (2010)

    Article  Google Scholar 

  23. Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 261–273. ACM (2015). https://doi.org/10.1145/2676726.2676987

  24. Giacobazzi, R., Mastroeni, I.: Abstract non-interference: a unifying framework for weakening information-flow. ACM Trans. Priv. Secur. 21(2), 9:1–9:31 (2018). https://doi.org/10.1145/3175660

  25. Giacobazzi, R., Mastroeni, I., Perantoni, E.: Adversities in abstract interpretation - accommodating robustness by abstract interpretation. ACM Trans. Program. Lang. Syst. 46(2), 5 (2024). https://doi.org/10.1145/3649309

    Article  Google Scholar 

  26. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000). https://doi.org/10.1145/333979.333989

    Article  MathSciNet  MATH  Google Scholar 

  27. Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pp. 11–20. IEEE Computer Society (1982). https://doi.org/10.1109/SP.1982.10014

  28. Grünbaum, B., Klee, V., Perles, M.A., Shephard, G.C.: Convex polytopes, vol. 16. Springer (1967)

    Google Scholar 

  29. Hunt, S., Mastroeni, I.: The PER model of abstract non-interference. In: Hankin, C., Siveroni, I. (eds.) Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3672, pp. 171–185. Springer (2005). https://doi.org/10.1007/11547662_13

  30. Liew, D., Cogumbreiro, T., Lange, J.: Sound and partially-complete static analysis of data-races in GPU programs. Proc. ACM Program. Lang. 8(OOPSLA2), 2434–2461 (2024). https://doi.org/10.1145/3689797

    Article  Google Scholar 

  31. Logozzo, F.: Towards a quantitative estimation of abstract interpretations. In: Workshop on Quantitative Analysis of Software. Microsoft (2009). https://www.microsoft.com/en-us/research/publication/towards-a-quantitative-estimation-of-abstract-interpretations/

  32. Mastroeni, I.: On the role of abstract non-interference in language-based security. In: Yi, K. (ed.) 3rd Asian Symp. on Programming Languages and Systems (APLAS ’05). Lecture Notes in Computer Science, vol. 3780, pp. 418–433. Springer

    Google Scholar 

  33. Mastroeni, I.: Abstract interpretation-based approaches to security - a survey on abstract non-interference and its challenging applications. Electron. Proc. Theoretical Comput. Sci. 129, 41–65 (2013). https://doi.org/10.4204/eptcs.129.4

    Article  MathSciNet  Google Scholar 

  34. Mastroeni, I.: Abstract local completeness - a local form of abstract non-interference. In: Krishna, S., Sankaranarayanan, S., Trivedi, A. (eds.) 26th Verification, Model Checking, and Abstract Interpretation (VMCAI 2025). Lecture Notes in Computer Science, vol. 15530, pp. 3–25. Springer (2025). https://doi.org/10.1007/978-3-031-82703-7_1

  35. Mastroeni, I., Pasqua, M.: Domain precision in galois connection-less abstract interpretation. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14284, pp. 434–459. Springer (2023). https://doi.org/10.1007/978-3-031-44245-2_19

  36. Mazzucato, D.: Static analysis by abstract interpretation of quantitative program properties. (Analyse Statique par Interprétation Abstraite de Propriétés Quantitatives de Programmes). Ph.D. thesis, École Normale Supérieure, Paris, France (2024). https://tel.archives-ouvertes.fr/tel-04886659

  37. Mazzucato, D., Campion, M., Urban, C.: Quantitative input usage static analysis. In: Benz, N., Gopinath, D., Shi, N. (eds.) NASA Formal Methods - 16th International Symposium, NFM 2024, Moffett Field, CA, USA, June 4-6, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14627, pp. 79–98. Springer (2024). https://doi.org/10.1007/978-3-031-60698-4_5

  38. Mazzucato, D., Campion, M., Urban, C.: Quantitative static timing analysis. In: Giacobazzi, R., Gorla, A. (eds.) Static Analysis - 31st International Symposium, SAS 2024, Pasadena, CA, USA, October 20-22, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14995, pp. 268–299. Springer (2024). https://doi.org/10.1007/978-3-031-74776-2_11

  39. Miné, A.: The octagon abstract domain. In: Burd, E., Aiken, P., Koschke, R. (eds.) Proc. of the 8th Working Conf. on Reverse Engineering, WCRE’01. p. 310. IEEE Computer Society (2001). https://doi.org/10.1109/WCRE.2001.957836

  40. O’Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL), 10:1–10:32 (2020). https://doi.org/10.1145/3371078

  41. Sotin, P.: Quantifying the precision of numerical abstract domains. Research Report (2010). https://inria.hal.science/inria-00457324

  42. Urban, C., Müller, P.: An abstract interpretation framework for input data usage. In: Ahmed, A. (ed.) 27th European Symposium on Programming, ESOP 2018. Lecture Notes in Computer Science, vol. 10801, pp. 683–710. Springer (2018). https://doi.org/10.1007/978-3-319-89884-1_24

Download references

Acknowledgements

This work was partially supported by the project SERICS (PE00000014) under the MUR National Recovery and Resilience Plan funded by the European Union - NextGenerationEU; by PRIN2022PNRR “RAP-ARA” (PE6) - codice MUR: P2022HXNSC; by the SAIF project, funded by the “France 2030” government investment plan managed by the French National Research Agency, under the reference ANR-23-PEIA-0006.

Author information

Authors and Affiliations

  1. Inria and ENS, PSL, Paris, France

    Marco Campion & Caterina Urban

  2. Department of Computer Science, University of Verona, Verona, Italy

    Isabella Mastroeni

Authors
  1. Marco Campion
    View author publications

    Search author on:PubMed Google Scholar

  2. Isabella Mastroeni
    View author publications

    Search author on:PubMed Google Scholar

  3. Caterina Urban
    View author publications

    Search author on:PubMed Google Scholar

Corresponding author

Correspondence to Marco Campion .

Editor information

Editors and Affiliations

  1. Korea University, Seoul, Korea (Republic of)

    Hakjoo Oh

  2. UNSW Sydney, Sydney, NSW, Australia

    Yulei Sui

Rights and permissions

Reprints and permissions

Copyright information

© 2026 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Campion, M., Mastroeni, I., Urban, C. (2026). Relating Distances and Abstractions. In: Oh, H., Sui, Y. (eds) Static Analysis. SAS 2025. Lecture Notes in Computer Science, vol 16100. Springer, Cham. https://doi.org/10.1007/978-3-032-07106-4_11

Download citation

Keywords

Publish with us

Policies and ethics