Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design

28-03-2023

On multi-language abstraction: Towards a static analysis of multi-language programs

Authors: Samuele Buro, Roy Crole, Isabella Mastroeni

Published in: Formal Methods in System Design

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Modern software development rarely takes place within a single programming language. Often, programmers appeal to cross-language interoperability. Examples are exploitation of novel features of one language within another, and cross-language code reuse. Our previous works developed a theory of so-called multi-languages, which arise by combining existing languages, defining a precise notion of (algebraic) multi-language semantics. As regards static analysis, the heterogeneity of the multi-language context opens up new and unexplored scenarios. In this paper, we provide a general theory for the combination of abstract interpretations of existing languages, regardless of their inherent nature, in order to gain an abstract semantics of multi-language programs. As a part of this general theory, we show that formal properties of interest of multi-language abstractions (e.g., soundness and completeness) boil down to the features of the interoperability mechanism that binds the underlying languages together. We extend many of the standard concepts of abstract interpretation to the framework of multi-languages.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
A commercial static code analyser for Java (version 3.2.0.1227: for Linux 64 bit).
 
Literature
1.
Ramsey N (2006) ML module mania: a type-safe, separately compiled, extensible interpreter. Electron Notes Theor Comput Sci 148(2):181–209CrossRef
2.
Juneau J, Baker J, Wierzbicki F, Soto L, Ng V (2010) The definitive guide to Jython: python for the java platform, 1st edn. Apress, BerkelyCrossRef
3.
Liang S (1999) Java native interface: programmer’s guide and reference, 1st edn. Addison-Wesley Longman Publishing Co. Inc., Boston
4.
Buro S, Mastroeni I (2019) On the multi-language construction. In: European symposium on programming. Springer, pp 293–321
5.
Chisnall D (2013) The challenge of cross-language interoperability. Commun ACM 56(12):50–56CrossRef
6.
Perconti JT, Ahmed A (2014) Verifying an open compiler using multi-language semantics. In: Proceedings of the 23rd European symposium on programming languages and systems, pp 128–148. Springer, Berlin
7.
Ahmed A, Blume M (2011) An equivalence-preserving cps translation via multi-language semantics. SIGPLAN Not 46(9):431–444CrossRefMATH
8.
Furr M, Foster JS (2005) Checking type safety of foreign function calls. SIGPLAN Not. 40(6):62–72CrossRef
9.
Gray KE (2008) Safe cross-language inheritance. In: Vitek J (ed) ECOOP 2008–object-oriented programming. Springer, Berlin, pp 52–75CrossRef
10.
Patterson D, Perconti J, Dimoulas C, Ahmed A (2017) Funtal: reasonably mixing a functional language with assembly. In: Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation. ACM, New York, pp 495–509
11.
Matthews J, Findler RB (2009) Operational semantics for multi-language programs. ACM Trans Program Lang Syst 31(3):12–11244CrossRefMATH
12.
Campbell G, Papapetrou PP (2013) SonarQube in action. Manning Publications Co., Shelter Island
13.
Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, pp 238–252
14.
15.
Buro S, Crole RL, Mastroeni I (2020) On multi-language abstraction—towards a static analysis of multi-language programs. In: Pichardie D, Sighireanu M (eds) Proceedings of static analysis—27th international symposium, SAS 2020, virtual event, November 18-20, 2020, Lecture Notes in Computer Science, vol 12389. Springer, pp 310–332
16.
Goguen JA, Meseguer J (1992) Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret Comput Sci 105(2):217–273MathSciNetCrossRefMATH
17.
18.
19.
Cohen H, Frey G, Avanzi R, Doche C, Lange T, Nguyen K, Vercauteren F (2005) Handbook of elliptic and hyperelliptic curve cryptography. CRC Press, Boca RatonCrossRefMATH
20.
21.
Cousot P, Giacobazzi R, Ranzato F (2019) A\(^2\)i: abstract\(^2\) interpretation. Proc ACM Program Lang 3(POPL):1–31CrossRef
22.
Amato G, Meo MC, Scozzari F (2020) On collecting semantics for program analysis. Theoret Comput Sci
23.
Spoto F, Jensen T (2003) Class analyses as abstract interpretations of trace semantics. ACM Trans Program Lang Syst 25(5):578–630CrossRef
24.
Bjørner N, Gurfinkel A (2015) Property directed polyhedral abstraction. In: International workshop on verification, model checking, and abstract interpretation. Springer, pp 263–281
25.
Kochems J, Ong C (2011) Improved functional flow and reachability analyses using indexed linear tree grammars. In: 22nd International conference on rewriting techniques and applications (RTA’11). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
26.
Giacobazzi R, Ranzato F (1997) Completeness in abstract interpretation: a domain perspective. In: International conference on algebraic methodology and software technology. Springer, pp 231–245
27.
Cousot P (2002) Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret Comput Sci 277(1–2):47–103MathSciNetCrossRefMATH
28.
Mastroeni I, Pasqua M (2017) Hyperhierarchy of semantics-a formal framework for hyperproperties verification. In: International static analysis symposium. Springer, pp 232–252
29.
Pasqua M (2019) Hyper static analysis of programs—an abstract interpretation-based framework for hyperproperties verification. PhD thesis, University of Verona
30.
Rival X, Yi K (2019) Introduction to Static Analysis
31.
Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on principles of programming languages, pp 84–96
32.
Arceri V, Mastroeni I (2019) Static program analysis for string manipulation languages. Electron Proc Theoret Comput Sci 299:19–33CrossRef
33.
34.
35.
36.
37.
Monat R, Ouadjaout A, Miné A (2021) A multilanguage static analysis of python programs with native C extensions. In: Dragoi C, Mukherjee S, Namjoshi KS (eds) Static analysis—28th international symposium, SAS 2021, USA. Lecture Notes in Computer Science, vol 12913, pp 323–345
38.
Gordon AD, Syme D (2001) Typing a multi-language intermediate code. Conference Record of POPL 2001: the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages. London, UK, January 17–19, 2001. ACM, New York, pp 248–260
39.
Grimmer M, Schatz R, Seaton C, Würthinger T, Luján M (2018) Cross-language interoperability in a multi-language runtime. ACM Trans Program Lang Syst 40(2):8–1843CrossRef
40.
Barrett E, Bolz CF, Tratt L (2015) Approaches to interpreter composition. Comput Lang Syst Struct 44:199–217
41.
42.
Buro S, Mastroeni I, Crole RL (2020) Equational logic and categorical semantics for multi-languages. In: In-press (accepted for Publication at 36th international conference on mathematical foundations of programming semantics—MFPS 2020)
43.
Buro S, Mastroeni I, Crole RL (2020) Equational logic and set-theoretic models for multi-languages. In: In-press (accepted for Publication at 21st Italian Conference on Theoretical Computer Science — ICTCS 2020)
44.
Tan G, Morrisett G (2007) Ilea: inter-language analysis across Java and C. SIGPLAN Not 42(10):39–56CrossRef
45.
Li S, Tan G (2014) Finding reference-counting errors in python/c programs with affine analysis. In: European conference on object-oriented programmings. Springer, pp 80–104
46.
47.
Li S, Tan G (2009) Finding bugs in exceptional situations of jni programs. In: Proceedings of the 16th ACM conference on computer and communications security, pp 442–452
48.
Cousot P (1997) Types as abstract interpretations. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 316–331
Metadata
Title
On multi-language abstraction: Towards a static analysis of multi-language programs
Authors
Samuele Buro
Roy Crole
Isabella Mastroeni
Publication date
28-03-2023
Publisher
Springer US
Published in
Formal Methods in System Design
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-022-00405-8

Premium Partner

    Image Credits