{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T17:38:21Z","timestamp":1758044301557,"version":"3.44.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032048479","type":"print"},{"value":"9783032048486","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T00:00:00Z","timestamp":1757376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T00:00:00Z","timestamp":1757376000000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-04848-6_2","type":"book-chapter","created":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T11:59:45Z","timestamp":1757678385000},"page":"22-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Smart Contracts in\u00a0Yul via\u00a0Transformation to\u00a0CHC by\u00a0Interpreter Specialization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7319-8439","authenticated-orcid":false,"given":"Emanuele","family":"De Angelis","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1268-7829","authenticated-orcid":false,"given":"Fabio","family":"Fioravanti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2109-8863","authenticated-orcid":false,"given":"Alejandro","family":"Hern\u00e1ndez-Cerezo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1316-2391","authenticated-orcid":false,"given":"Giulia","family":"Matricardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,9]]},"reference":[{"key":"2_CR1","unstructured":"Akhunov, A., Salem, M.: EIP-1153: Transient storage opcodes (2018). https:\/\/eips.ethereum.org\/EIPS\/eip-1153. Ethereum Improvement Proposals, no. 1153"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Correas, J., Gordillo, P., Rom\u00e1n-D\u00edez, G., Rubio, A.: SAFEVM: a safety verifier for Ethereum smart contracts. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 386\u2013389 (2019)","DOI":"10.1145\/3293882.3338999"},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"2256","DOI":"10.1109\/TDSC.2022.3178836","volume":"20","author":"E Albert","year":"2023","unstructured":"Albert, E., Grossman, S., Rinetzky, N., Rodr\u00edguez-N\u00fa\u00f1ez, C., Rubio, A., Sagiv, M.: Relaxed effective callback freedom: a parametric correctness condition for sequential modules with callbacks. IEEE Trans. Dependable Secur. Comput. 20(3), 2256\u20132273 (2023)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: solidity compiler\u2019s model checker. In: Computer Aided Verification (CAV), vol. 13371 of LNCS, pp. 325\u2013338. Springer, Heidelberg (2022)","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/j.scico.2016.11.002","volume":"147","author":"E De Angelis","year":"2017","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions via program specialization. Sci. Comput. Program. 147, 78\u2013108 (2017)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"2_CR6","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)","journal-title":"Theory Pract. Log. Program."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-642-54862-8_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E De Angelis","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: VeriMAP: a tool for verifying programs through transformations. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 568\u2013574. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_47"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"De\u00a0Angelis, E., Krishnan, H.G.V.: Competition of solvers for constrained horn clauses (CHC-COMP 2023). In: TOOLympics Challenge 2023, pp. 38\u201351. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-67695-6_2"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Dxo, M.S., Paraskevopoulou, Z., Lundfall, M., Brockman, M.: Hevm, a fast symbolic execution framework for EVM bytecode. In: Computer Aided Verification (CAV), vol. 14681 of LNCS, pp. 453\u2013465. Springer, Heidelberg (2024)","DOI":"10.1007\/978-3-031-65627-9_22"},{"issue":"4","key":"2_CR10","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1023\/A:1010095604496","volume":"12","author":"Y Futamura","year":"1999","unstructured":"Futamura, Y.: Partial evaluation of computation process - an approach to a compiler-compiler. High. Order Symb. Comput. 12(4), 381\u2013391 (1999)","journal-title":"High. Order Symb. Comput."},{"issue":"10","key":"2_CR11","doi-asserted-by":"publisher","first-page":"1409","DOI":"10.1016\/j.infsof.2009.04.010","volume":"51","author":"M G\u00f3mez-Zamalloa","year":"2009","unstructured":"G\u00f3mez-Zamalloa, M., Albert, E., Puebla, G.: Decompilation of java bytecode to prolog by partial evaluation. Inf. Softw. Technol. 51(10), 1409\u20131427 (2009)","journal-title":"Inf. Softw. Technol."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Formal Methods in Computer Aided Design, pp. 1\u20137. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"2_CR13","unstructured":"Jackson, D., Nandi, C., Sagiv, M.: Certora Technology White Paper (2022). https:\/\/docs.certora.com\/en\/latest\/docs\/whitepaper\/index.html"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\u201320","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Logic Program. 19\u201320, 503\u2013581 (1994)","journal-title":"J. Logic Program."},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Lin, Y.Y., Tzevelekos, N.: An operational semantics for yul. In: Software Engineering and Formal Methods, pp. 328\u2013346. Springer, Heidelberg (2024)","DOI":"10.1007\/978-3-031-77382-2_19"},{"key":"2_CR17","unstructured":"OpenZeppelin. PaymentSplitter Contract. https:\/\/docs.openzeppelin.com\/contracts\/4.x\/api\/finance#PaymentSplitter"},{"issue":"2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3564699","volume":"26","author":"R Otoni","year":"2023","unstructured":"Otoni, R., Marescotti, M., Alt, L., Eugster, P., Hyv\u00e4rinen, A., Sharygina, N.: A solicitous approach to smart contract verification. ACM Trans. Priv. Secur. 26(2), 1\u201328 (2023)","journal-title":"ACM Trans. Priv. Secur."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Rosu, G.: A formal verification tool for Ethereum VM bytecode. In: ACM Joint Meeting on European Software Engineering Conf. and Symposium on the Foundations of Software Engineering, pp. 912\u2013915. ACM (2018)","DOI":"10.1145\/3236024.3264591"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-49727-7_15","volume-title":"Static Analysis","author":"JC Peralta","year":"1998","unstructured":"Peralta, J.C., Gallagher, J.P., Sa\u011flam, H.: Analysis of imperative programs through analysis of constraint logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 246\u2013261. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49727-7_15"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Rastello, F., Bouchez-Tichadou, F. (eds.): SSA-based Compiler Design. Springer, Heidelberg (2022)","DOI":"10.1007\/978-3-030-80515-9"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"So, S., Lee, M., Park, J., Lee, H., Oh, H.: VERISMART: a highly precise safety verifier for ethereum smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 1678\u20131694 (2020)","DOI":"10.1109\/SP40000.2020.00032"},{"key":"2_CR23","unstructured":"Solidity Team. Solidity Documentation. Release 0.8.30 (2025). https:\/\/docs.soliditylang.org\/_\/downloads\/en\/v0.8.30\/pdf\/"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-030-94583-1_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Wesley","year":"2022","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R., W\u00fcstholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstraction in SmartACE. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 425\u2013449. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21"},{"issue":"2014","key":"2_CR25","first-page":"1","volume":"151","author":"G Wood","year":"2014","unstructured":"Wood, G., et al.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Paper 151(2014), 1\u201332 (2014)","journal-title":"Ethereum Proj. Yellow Paper"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04848-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T11:59:48Z","timestamp":1757678388000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04848-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,9]]},"ISBN":["9783032048479","9783032048486"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04848-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,9]]},"assertion":[{"value":"9 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rende","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lopstr.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}