Skip to main content
SpringerLink
Log in

On Constructivity of Galois Connections

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10747))

  • 951 Accesses

Abstract

Abstract interpretation-based static analyses rely on abstract domains of program properties, such as intervals or congruences for integer variables. Galois connections (GCs) between posets provide the most widespread and useful formal tool for mathematically specifying abstract domains. Darais and Van Horn [2016] put forward a notion of constructive Galois connection for unordered sets (rather than posets), which allows to define abstract domains in a so-called mechanized and calculational proof style and therefore enables the use of proof assistants like Coq and Agda for automatically extracting certified algorithms of static analysis. We show here that constructive GCs are isomorphic, in a mathematical meaning which includes sound abstract functions, to so-called partitioning GCs — an already known class of GCs which allows to cast standard set partitions as an abstract domain. Darais and Van Horn [2016] further provide a notion of constructive Galois connection for posets, which we prove to be mathematically isomorphic to plain GCs. Drawing on these findings, we put forward purely partitioning GCs, a novel class of constructive abstract domains for a mechanized approach to abstract interpretation. We show that this class of abstract domains allows us to represent a set partition in a flexible way while retaining a constructive approach to Galois connections.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a C value analysis based on abstract interpretation. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 324–344. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_18

    Chapter  Google Scholar 

  2. Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)

    Google Scholar 

  3. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1–2), 47–103 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM POPL, pp. 238–252 (1977)

    Google Scholar 

  5. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th ACM POPL, pp. 269–282 (1979)

    Google Scholar 

  6. Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic and Computation 2(4), 511–547 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages) (Invited Paper). In: Proc. of the IEEE Int. Conf. on Computer Languages (ICCL 1994), pp. 95–112. IEEE Computer Society Press (1994)

    Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation of algebraic polynomial systems (extended abstract). In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 138–154. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0000468

    Chapter  Google Scholar 

  9. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. 5th ACM POPL, pp. 84–97 (1978)

    Google Scholar 

  10. Darais, D., Van Horn, D.: Constructive Galois connections: taming the Galois connection framework for mechanized metatheory. In: Proceedings of the 21st ACM Intern. Conf. on Functional Programming (ICFP 2016), pp. 311–324. ACM (2016)

    Google Scholar 

  11. Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comp. Program. 32, 177–210 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  12. Giacobazzi, R., Ranzato, F.: Example-Guided abstraction simplification. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 211–222. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14162-1_18

    Chapter  Google Scholar 

  13. Giacobazzi, R., Ranzato, F.: Correctness kernels of abstract interpretations. Information and Computation 237, 187–203 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  14. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. Jourdan, J.H.: Verasco: A Formally Verified C Static Analyzer. PhD thesis, Université Paris Diderot (Paris 7), France (2016)

    Google Scholar 

  16. Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Proc. 42nd ACM POPL, pp. 247–259 (2015)

    Google Scholar 

  17. Midtgaard, J., Jensen, T.: A calculational approach to control-flow analysis by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 347–362. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69166-2_23

    Chapter  Google Scholar 

  18. Monniaux, D.: Réalisation Mécanisée d’Interpréteurs Abstraits. Université Paris VII, France, Rapport de DEA (1998) (in French)

    Google Scholar 

  19. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)

    Google Scholar 

  20. Pichardie, D.: Interprétation Abstraite en Logique Intuitionniste: Extraction d’Analyseurs Java Certifiés. PhD thesis, Université de Rennes, France (2005) (in French)

    Google Scholar 

  21. Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24725-8_3

    Chapter  Google Scholar 

  22. Ranzato, F., Tapparo, F.: An abstract interpretation-based refinement algorithm for strong preservation. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 140–156. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_10

    Chapter  Google Scholar 

  23. Ranzato, F., Tapparo, F.: Generalized strong preservation by abstract interpretation. J. Logic and Computation 17(1), 157–197 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  24. Silva, P.F., Oliveira, P.F.: ‘Galculator’:functional prototype of a Galois-connection based proof assistant. In: Proc. 10th International ACM Conference on Principles and Practice of Declarative Programming (PPDP 2008), pp. 44–55. ACM (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Matematica, University of Padova, Padova, Italy

    Francesco Ranzato

Authors
  1. Francesco Ranzato
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesco Ranzato .

Editor information

Editors and Affiliations

  1. University of Texas , Austin, Texas, USA

    Isil Dillig

  2. University of California , Los Angeles, California, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ranzato, F. (2018). On Constructivity of Galois Connections. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-73721-8_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-73720-1

  • Online ISBN: 978-3-319-73721-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation