{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T06:58:32Z","timestamp":1778309912164,"version":"3.51.4"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"name":"SERICS","award":["PE00000014"],"award-info":[{"award-number":["PE00000014"]}]},{"name":"iNEST","award":["ECS 00000043"],"award-info":[{"award-number":["ECS 00000043"]}]},{"name":"PNRR NextGeneration EU, and Bando di Ateneo per la Ricerca 2022"},{"DOI":"10.13039\/501100004770","name":"University of Parma","doi-asserted-by":"crossref","award":["MUR_DM737_2022_FIL_PROGETTI_B_ARCERI_COFIN, CUP: D91B21005370003"],"award-info":[{"award-number":["MUR_DM737_2022_FIL_PROGETTI_B_ARCERI_COFIN, CUP: D91B21005370003"]}],"id":[{"id":"10.13039\/501100004770","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Distrib. Ledger Technol."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>\n            Once deployed in blockchain, smart contracts become immutable: Attackers can exploit bugs and vulnerabilities in their code that cannot be replaced with a bug-free version. For this reason, the verification of smart contracts\n            <jats:italic>before<\/jats:italic>\n            they are deployed in blockchain is important. However, the development of verification tools is not easy, especially if one wants to obtain guarantees by using formal methods. This article describes the development, from scratch, of a static analyzer based on abstract interpretation for the verification of real-world Tezos smart contracts. The analyzer is generic with respect to the property under analysis. This article shows taint analysis as a concrete instantiation of the analyzer, at different levels of precision, to detect untrusted cross-contract invocations.\n          <\/jats:p>","DOI":"10.1145\/3643567","type":"journal-article","created":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T12:38:38Z","timestamp":1706531918000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Design and Implementation of Static Analyses for Tezos Smart Contracts"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8074-8980","authenticated-orcid":false,"given":"Luca","family":"Olivieri","sequence":"first","affiliation":[{"name":"Ca\u2019 Foscari University of Venice, Venezia, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9930-8854","authenticated-orcid":false,"given":"Luca","family":"Negrini","sequence":"additional","affiliation":[{"name":"Ca\u2019 Foscari University of Venice, Venezia, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5150-0393","authenticated-orcid":false,"given":"Vincenzo","family":"Arceri","sequence":"additional","affiliation":[{"name":"University of Parma, Parma, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4064-7170","authenticated-orcid":false,"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[{"name":"INRIA, Rennes, France and University of Copenhagen, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2973-0384","authenticated-orcid":false,"given":"Fausto","family":"Spoto","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"1","volume-title":"Proceedings of a Symposium on Compiler Optimization","author":"Allen Frances E.","year":"1970","unstructured":"Frances E. Allen. 1970. Control flow analysis. In Proceedings of a Symposium on Compiler Optimization (Urbana-Champaign, Illinois). Association for Computing Machinery, New York, NY, 1\u201319. DOI:10.1145\/800028.808479"},{"key":"e_1_3_2_3_2","volume-title":"Mastering Ethereum: Building Smart Contracts and Dapps","author":"Antonopoulos A. M.","year":"2018","unstructured":"A. M. Antonopoulos and G. Wood. 2018. Mastering Ethereum: Building Smart Contracts and Dapps. O\u2019Reilly, Sebastopol."},{"key":"e_1_3_2_4_2","unstructured":"ArcheType. 2023. Retrieved April 2023 from https:\/\/archetype-lang.org\/"},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Pedro Arrojado da Horta Jo\u00e3o Santos Reis M\u00e1rio Pereira and Sim\u00e3o Melo de Sousa. 2020. WhylSon: Proving your Michelson smart contracts in why3. arXiv:2005.14650 [cs.PL].","DOI":"10.1109\/Blockchain50366.2020.00059"},{"key":"e_1_3_2_6_2","volume-title":"Proceedings of the 11th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP\u201922, San Diego, CA, USA)","author":"Bau G.","year":"2022","unstructured":"G. Bau, A. Min\u00e9, V. Botbol, and M. Bouaziz. 2022. Abstract interpretation of Michelson smart-contracts. In Proceedings of the 11th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP\u201922, San Diego, CA, USA). Association for Computing Machinery, New York, NY, 36\u201343. 10.1145\/3520313.3534660"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","unstructured":"Bruno Bernardo Rapha\u00ebl Cauderlier Guillaume Claret Arvid Jakobsson Basile Pesin and Julien Tesson. 2020. Making Tezos smart contracts more reliable with Coq. In Leveraging Applications of Formal Methods Verification and Validation: Applications Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing Cham 60\u201372.","DOI":"10.1007\/978-3-030-61467-6_5"},{"key":"e_1_3_2_8_2","unstructured":"Alessandro Brighente Mauro Conti and Sathish Kumar. 2022. Extorsionware: Exploiting smart contract vulnerabilities for fun and profit. arXiv:2203.09843. Retrieved from https:\/\/arxiv.org\/abs\/2203.09843"},{"key":"e_1_3_2_9_2","volume-title":"Extorsionware: Bringing Ransomware Attacks to Blockchain Smart Contracts","author":"Cattai Christian","year":"2021","unstructured":"Christian Cattai. 2021. Extorsionware: Bringing Ransomware Attacks to Blockchain Smart Contracts. Master thesis. University of Padua. https:\/\/hdl.handle.net\/20.500.12608\/33778"},{"key":"e_1_3_2_10_2","volume-title":"Secure Programming with Static Analysis","author":"Chess Brian","year":"2007","unstructured":"Brian Chess and Jacob West. 2007. Secure Programming with Static Analysis. Addison-Wesley Professional, Boston."},{"key":"e_1_3_2_11_2","unstructured":"CosmWasm. 2023. CosmWasm Book. Retrieved November 2023 from https:\/\/book.cosmwasm.com\/"},{"key":"e_1_3_2_12_2","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press, Cambridge."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"P. Cousot and R. Cousot. 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 (Los Angeles California) (POPL\u201977). Association for Computing Machinery New York NY 238\u2013252. 10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"P. Cousot and R. Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages (San Antonio Texas) (POPL\u201979). Association for Computing Machinery New York NY 269\u2013282. 10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_16_2","volume-title":"Structured Programming","author":"Dahl O. J.","year":"1972","unstructured":"O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare (Eds.). 1972. Structured Programming. Academic Press Ltd., Gbr."},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","unstructured":"Delphine Demange Thomas Jensen and David Pichardie. 2010. A provably correct stackless intermediate representation for Java bytecode. In Proceedings of the 8th Asian Conference on Programming Languages and Systems (Shanghai China) (APLAS\u201910). Springer-Verlag Berlin Heidelberg 97\u2013113.","DOI":"10.1007\/978-3-642-17164-2_8"},{"issue":"5","key":"e_1_3_2_18_2","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/360051.360056","article-title":"A lattice model of secure information flow","volume":"19","author":"Denning D. E.","year":"1976","unstructured":"D. E. Denning. 1976. A lattice model of secure information flow. Commun. ACM 19, 5 (1976), 236\u2013243.","journal-title":"Commun. ACM"},{"key":"e_1_3_2_19_2","unstructured":"EOS.IO. 2023. EOS.IO Developer\u2014Manual. Retrieved April 2023 from https:\/\/developers.eos.io\/welcome\/v2.1\/manuals\/index"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Michael D. Ernst A. Lovato D. Macedonio C. Spiridon and F. Spoto. 2015. Boolean formulas for the static identification of injection attacks in Java. In Proceedings of the 20th International Conference on Logic for Programming Artificial Intelligence and Reasoning - Volume 9450 (Suva Fiji) (LPAR-20 2015). Springer-Verlag Berlin Heidelberg 130\u2013145. 10.1007\/978-3-662-48899-7_10","DOI":"10.1007\/978-3-662-48899-7_10"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"P. Ferrara L. Negrini V. Arceri and A. Cortesi. 2021. Static analysis for dummies: Experiencing LiSA. In 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (Virtual Canada) (SOAP 2021). Association for Computing Machinery New York NY 1\u20136.","DOI":"10.1145\/3460946.3464316"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Pietro Ferrara Luca Olivieri and Fausto Spoto. 2020. Backflow: Backward context-sensitive flow reconstruction of taint analysis results. In Verification Model Checking and Abstract Interpretation: 21st International Conference VMCAI 2020 New Orleans LA USA January 16\u201321 2020 Proceedings (New Orleans LA USA). Springer-Verlag Berlin Heidelberg 23\u201343. 10.1007\/978-3-030-39322-9_2","DOI":"10.1007\/978-3-030-39322-9_2"},{"issue":"7","key":"e_1_3_2_23_2","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1142\/S0218194021500303","article-title":"Static privacy analysis by flow reconstruction of tainted data","volume":"31","author":"Ferrara P.","year":"2021","unstructured":"P. Ferrara, L. Olivieri, and F. Spoto. 2021. Static privacy analysis by flow reconstruction of tainted data. Int. J. Softw. Eng. Knowl. Eng. 31, 7 (2021), 973\u20131016.","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"e_1_3_2_24_2","article-title":"Tezos\u2014A self-amending crypto-ledger","author":"Goodman L. M.","year":"2014","unstructured":"L. M. Goodman. 2014. Tezos\u2014A self-amending crypto-ledger. (White paper). Retrieved April 2023 from https:\/\/tezos.com\/whitepaper.pdf. Accessed 04\/2023.","journal-title":"https:\/\/tezos.com\/whitepaper.pdf"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Bo Jiang Ye Liu and W.K. Chan. 2018. ContractFuzzer: Fuzzing smart contracts for vulnerability detection. In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering (Montpellier France) (ASE\u201918). Association for Computing Machinery New York NY 259\u2013269. 10.1145\/3238147.3238177","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_3_2_26_2","article-title":"Michelson Reference\u2014TRANSFER_TOKENS","author":"Labs Nomadic","year":"2020","unstructured":"Nomadic Labs. 2020. Michelson Reference\u2014TRANSFER_TOKENS. https:\/\/tezos.gitlab.io\/michelson-reference\/#instr-TRANSFER_TOKENS. Accessed 04\/2023.","journal-title":"https:\/\/tezos.gitlab.io\/michelson-reference\/#instr-TRANSFER_TOKENS"},{"key":"e_1_3_2_27_2","article-title":"Michelson Reference\u2013Typing and Semantics Rules","author":"Labs Nomadic","year":"2020","unstructured":"Nomadic Labs. 2020. Michelson Reference\u2013Typing and Semantics Rules. Retrieved April 2023 from https:\/\/tezos.gitlab.io\/michelson-reference\/#typing-and-semantics-rules. Accessed 04\/2023.","journal-title":"https:\/\/tezos.gitlab.io\/michelson-reference\/#typing-and-semantics-rules"},{"key":"e_1_3_2_28_2","unstructured":"LIGO. 2023. LIGO Documentation. Retrieved April 2023 from https:\/\/ligolang.org\/"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-540-78791-4_14","volume-title":"Compiler Construction","author":"Logozzo Francesco","year":"2008","unstructured":"Francesco Logozzo and Manuel F\u00e4hndrich. 2008. On the relative completeness of bytecode analysis versus source code analysis. In Compiler Construction, Laurie Hendren (Ed.). Springer, Berlin, 197\u2013212."},{"key":"e_1_3_2_30_2","unstructured":"Bertrand Meyer. 2019. Soundness and Completeness: With Precision BLOGCACM. Retrieved April 2023 from https:\/\/cacm.acm.org\/blogs\/blog-cacm\/236068-soundness-and-completeness-with-precision\/fulltext. Accessed: 04\/2023."},{"key":"e_1_3_2_31_2","volume-title":"Proceedings of the 4th International Workshop on Formal Methods for Blockchains (FMBC\u201922) (Open Access Series in Informatics (OASIcs), Vol. 105)","author":"Milo Mikkel","year":"2022","unstructured":"Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. 2022. Finding smart contract vulnerabilities with concert\u2019s property-based testing framework. In Proceedings of the 4th International Workshop on Formal Methods for Blockchains (FMBC\u201922) (Open Access Series in Informatics (OASIcs), Vol. 105), Zaynah Dargaye and Clara Schneidewind (Eds.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 2:1\u20132:13. 10.4230\/OASIcs.FMBC.2022.2"},{"key":"e_1_3_2_32_2","volume-title":"Proceedings of the 9th Workshop on Tools for Automatic Program Analysis","author":"Min\u00e9 A.","year":"2018","unstructured":"A. Min\u00e9, A. Ouadjaout, and M. Journault. 2018. Design of a modular platform for static analysis. In Proceedings of the 9th Workshop on Tools for Automatic Program Analysis. 1\u20135."},{"key":"e_1_3_2_33_2","unstructured":"Dominik Muhs. 2023. SWC Registry\u2014Delegatecall to Untrusted Callee. Retrieved October 2023 from https:\/\/swcregistry.io\/docs\/SWC-112\/. Accessed: 10\/2023."},{"key":"e_1_3_2_34_2","volume-title":"A Generic Framework for Multilanguage Analysis","author":"Negrini Luca","year":"2023","unstructured":"Luca Negrini. 2023. A Generic Framework for Multilanguage Analysis. Ph. D. Dissertation. Universit\u00e1 Ca\u2019 Foscari Venezia."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-19-9601-6_2"},{"key":"e_1_3_2_36_2","first-page":"8","volume-title":"Proceedings of the 12th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP\u201923)","author":"Negrini Luca","year":"2023","unstructured":"Luca Negrini, Guruprerana Shabadi, and Caterina Urban. 2023. Static analysis of data transformations in jupyter notebooks. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP\u201923). Association for Computing Machinery, New York, NY, 8\u201313. DOI:10.1145\/3589250.3596145"},{"key":"e_1_3_2_37_2","unstructured":"Neo Team. 2023. NEO Documentation\u2014Smart Contracts. Retrieved April 2023 from https:\/\/neo.org\/technology#smart-contracts"},{"issue":"2","key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s00354-022-00167-1","article-title":"Helmholtz: A verifier for Tezos smart contracts based on refinement types","volume":"40","author":"Nishida Y.","year":"2022","unstructured":"Y. Nishida, H. Saito, R. Chen, A. Kawata, J. Furuse, K. Suenaga, and A. Igarashi. 2022. Helmholtz: A verifier for Tezos smart contracts based on refinement types. New Gener. Comput. 40, 2 (2022), 507\u2013540.","journal-title":"New Gener. Comput."},{"key":"e_1_3_2_39_2","unstructured":"Nomadic Labs. 2023. Michelson: The Language of Smart Contracts in Tezos. Retrieved April 2023 from https:\/\/tezos.gitlab.io\/active\/michelson.html#michelson-the-language-of-smart-contracts-in-tezos. Accessed 04\/2023."},{"issue":"3","key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"1864","DOI":"10.1007\/s10664-019-09796-5","article-title":"An exploratory study of smart contracts in the ethereum blockchain platform","volume":"25","author":"Oliva G. A.","year":"2020","unstructured":"G. A. Oliva, A. E. Hassan, and Z. M. Jiang. 2020. An exploratory study of smart contracts in the ethereum blockchain platform. Empir. Softw. Eng. 25, 3 (2020), 1864\u20131904.","journal-title":"Empir. Softw. Eng."},{"key":"e_1_3_2_41_2","first-page":"80","volume-title":"Proceedings of the IEEE International Conference on Pervasive Computing and Communications Workshops and Other Affiliated Events (PerCom Workshops\u201923)","author":"Olivieri Luca","year":"2023","unstructured":"Luca Olivieri, Thomas Jensen, Luca Negrini, and Fausto Spoto. 2023. MichelsonLiSA: A static analyzer for tezos. In Proceedings of the IEEE International Conference on Pervasive Computing and Communications Workshops and Other Affiliated Events (PerCom Workshops\u201923). 80\u201385. DOI:10.1109\/PerComWorkshops56833.2023.10150247"},{"key":"e_1_3_2_42_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"23:1\u201323:25","volume-title":"Proceedings of the 37th European Conference on Object-Oriented Programming (ECOOP\u201923),","volume":"263","author":"Olivieri Luca","year":"2023","unstructured":"Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, and Fausto Spoto. 2023. Information flow analysis for detecting non-determinism in blockchain. In Proceedings of the 37th European Conference on Object-Oriented Programming (ECOOP\u201923),Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, 23:1\u201323:25. DOI:10.4230\/LIPIcs.ECOOP.2023.23"},{"key":"e_1_3_2_43_2","volume-title":"Proceedings of the 11th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP\u201922, San Diego, CA, USA)","author":"Olivieri L.","year":"2022","unstructured":"L. Olivieri, F. Tagliaferro, V. Arceri, M. Ruaro, L. Negrini, A. Cortesi, P. Ferrara, F. Spoto, and E. Talin. 2022. Ensuring determinism in blockchain software with GoLiSA: an industrial experience report. In Proceedings of the 11th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis (SOAP\u201922, San Diego, CA, USA). Association for Computing Machinery, New York, NY, 23\u201329. 10.1145\/3520313.3534658"},{"key":"e_1_3_2_44_2","unstructured":"OpenZeppelin. 2023. Proxy Upgrade Pattern. Retrieved October 2023 from https:\/\/docs.openzeppelin.com\/upgrades-plugins\/1.x\/proxies. Accessed 10\/2023."},{"key":"e_1_3_2_45_2","article-title":"Mythril Wiki Page","author":"Parasaram Nikhil","year":"2020","unstructured":"Nikhil Parasaram. 2020. Mythril Wiki Page. Retrieved April 2023 from https:\/\/github.com\/ConsenSys\/mythril\/wiki. Accessed 04\/2023.","journal-title":"https:\/\/github.com\/ConsenSys\/mythril\/wiki"},{"key":"e_1_3_2_46_2","unstructured":"Parity Technologies. 2023. Ink! Documentation. Retrieved April 2023 from https:\/\/paritytech.github.io\/ink-docs\/why-rust-for-smart-contracts. Accessed 04\/2023."},{"key":"e_1_3_2_47_2","unstructured":"T. Parr. 2023. ANTLR Website. Retrieved April 2023 from https:\/\/www.antlr.org\/"},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1145\/1993498.1993548","volume-title":"Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201911)","author":"Parr Terence","year":"2011","unstructured":"Terence Parr and Kathleen Fisher. 2011. LL(*): The foundation of the ANTLR parser generator. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201911). Association for Computing Machinery, New York, NY, 425\u2013436. DOI:10.1145\/1993498.1993548"},{"key":"e_1_3_2_49_2","unstructured":"Jo\u00e3o Santos Reis. 2022. Tezla Test Repository. Retrieved April 2023 from https:\/\/github.com\/joaosreis\/tezla\/tree\/main\/tests.Commit:baacf2a79f8ac1fee8b5200395ffc14d5b9922e6. Accessed 04\/2023."},{"key":"e_1_3_2_50_2","series-title":"OpenAccess Series in Informatics (OASIcs)","first-page":"4:1\u20134:12","volume-title":"Proceedings of the 2nd Workshop on Formal Methods for Blockchains (FMBC\u201920)","volume":"84","author":"Reis Jo\u00e3o Santos","year":"2020","unstructured":"Jo\u00e3o Santos Reis, Paul Crocker, and Sim\u00e3o Melo de Sousa. 2020. Tezla, an intermediate representation for static analysis of michelson smart contracts. In Proceedings of the 2nd Workshop on Formal Methods for Blockchains (FMBC\u201920)OpenAccess Series in Informatics (OASIcs), Vol. 84. 4:1\u20134:12. DOI:10.4230\/OASIcs.FMBC.2020.4"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1090\/s0002-9947-1953-0053041-6"},{"key":"e_1_3_2_52_2","volume-title":"Introduction to Static Analysis: An Abstract Interpretation Perspective","author":"Rival Xavier","year":"2020","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, Cambridge."},{"issue":"1","key":"e_1_3_2_53_2","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","article-title":"Language-based information-flow security","volume":"21","author":"Sabelfeld A.","year":"2003","unstructured":"A. Sabelfeld and A. C. Myers. 2003. Language-based information-flow security. IEEE J. Sel. Areas Commun. 21, 1 (2003), 5\u201319.","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"e_1_3_2_54_2","unstructured":"SmartPy. 2023. Retrieved April 2023 from https:\/\/smartpy.io\/docs\/"},{"key":"e_1_3_2_55_2","unstructured":"SmartPy. 2023. SmartPy Reference\u2014Constants vs Expressions. Retrieved April 2023 from https:\/\/smartpy.io\/reference.html. Accessed: 04\/2023."},{"key":"e_1_3_2_56_2","unstructured":"Solana. 2023. Solana Getting Started with Solana Development. Retrieved April 2023 from https:\/\/solana.com\/news\/getting-started-with-solana-development. Accessed: 04\/2023."},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-662-53413-7_3","volume-title":"Static Analysis","author":"Spoto Fausto","year":"2016","unstructured":"Fausto Spoto. 2016. The julia static analyzer for Java. In Static Analysis, Xavier Rival (Ed.). Springer, Berlin, 39\u201357."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54455-3_40"},{"issue":"3","key":"e_1_3_2_59_2","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/3332371","article-title":"Static identification of injection attacks in Java","volume":"41","author":"Spoto F.","year":"2019","unstructured":"F. Spoto, E. Burato, M. D. Ernst, P. Ferrara, A. Lovato, D. Macedonio, and C. Spiridon. 2019. Static identification of injection attacks in Java. ACM Trans. Program. Lang. Syst. 41, 3, Article 18 (Jul.2019), 58 pages.","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"e_1_3_2_60_2","first-page":"148","article-title":"A survey of smart contract formal specification and verification","volume":"54","author":"Tolmach Palina","year":"2021","unstructured":"Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu, and Zengxiang Li. 2021. A survey of smart contract formal specification and verification. ACM Comput. Surv. 54, 7, Article 148 (2021), 38 pages.","journal-title":"ACM Comput. Surv."},{"key":"e_1_3_2_61_2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/1542476.1542486","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201909)","author":"Tripp Omer","year":"2009","unstructured":"Omer Tripp, Marco Pistoia, Stephen J. Fink, Manu Sridharan, and Omri Weisman. 2009. TAJ: Effective taint analysis of web applications. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201909), Michael Hind and Amer Diwan (Eds.). ACM, New York, NY, 87\u201397. DOI:10.1145\/1542476.1542486"},{"key":"e_1_3_2_62_2","first-page":"34","volume-title":"Proceedings of the IEEE International Conference on Advances in Electrical Engineering and Computer Applications (AEECA\u201922)","author":"Wang Xiaoqiang","year":"2022","unstructured":"Xiaoqiang Wang, Jianhua Li, and Xuesen Zhang. 2022. A semantic-based smart contract defect detection general platform. In Proceedings of the IEEE International Conference on Advances in Electrical Engineering and Computer Applications (AEECA\u201922). 34\u201337. DOI:10.1109\/AEECA55500.2022.9918903"},{"key":"e_1_3_2_63_2","first-page":"23","volume-title":"Proceedings of the IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER\u201920)","author":"Zhang Yuyao","year":"2020","unstructured":"Yuyao Zhang, Siqi Ma, Juanru Li, Kailai Li, Surya Nepal, and Dawu Gu. 2020. SMARTSHIELD: Automatic smart contract protection made easy. In Proceedings of the IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER\u201920). 23\u201334. DOI:10.1109\/SANER48275.2020.9054825"}],"container-title":["Distributed Ledger Technologies: Research and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643567","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T12:38:49Z","timestamp":1749818329000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643567"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,13]]},"references-count":62,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3643567"],"URL":"https:\/\/doi.org\/10.1145\/3643567","relation":{},"ISSN":["2769-6480","2769-6480"],"issn-type":[{"value":"2769-6480","type":"print"},{"value":"2769-6480","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,13]]},"assertion":[{"value":"2023-04-22","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-11","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}