{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T04:14:42Z","timestamp":1768277682928,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031765537","type":"print"},{"value":"9783031765544","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_14","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:17:57Z","timestamp":1731410277000},"page":"256-266","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Solvent: Liquidity Verification of\u00a0Smart Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3796-9774","authenticated-orcid":false,"given":"Massimo","family":"Bartoletti","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8711-4670","authenticated-orcid":false,"given":"Angelo","family":"Ferrando","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0009-0428-4403","authenticated-orcid":false,"given":"Enrico","family":"Lipparini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6138-4229","authenticated-orcid":false,"given":"Vadim","family":"Malvone","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"14_CR1","unstructured":"SMTChecker and formal verification: contract balance (2023). https:\/\/docs.soliditylang.org\/en\/v0.8.24\/smtchecker.html#contract-balance"},{"key":"14_CR2","unstructured":"An open benchmark for evaluating smart contracts verification tools (2024). https:\/\/github.com\/fsainas\/contracts-verification-benchmark"},{"key":"14_CR3","unstructured":"Alois, J.: Ethereum Parity hack may impact ETH 500,000 or \\$146 million (2017). https:\/\/www.crowdfundinsider.com\/2017\/11\/124200-ethereum-parity-hack-may-impact-eth-500000-146-million\/. Accessed 9 Apr 2024"},{"key":"14_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-031-13185-1_16","volume-title":"Computer Aided Verification","author":"L Alt","year":"2022","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: solidity compiler\u2019s model checker. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 325\u2013338. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","volume-title":"Principles of Security and Trust","author":"N Atzei","year":"2017","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"14_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). https:\/\/smtlib.cs.uiowa.edu\/language.shtml"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability (2021). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"14_CR10","unstructured":"Bartoletti, M., Ferrando, A., Lipparini, E., Malvone, V.: Solvent: liquidity verification of smart contracts. https:\/\/github.com\/AngeloFerrando\/Solvent"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Ferrando, A., Lipparini, E., Malvone, V.: Solvent: liquidity verification of smart contracts. CoRR abs\/2404.17864 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2404.17864","DOI":"10.48550\/ARXIV.2404.17864"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Fioravanti, F., Matricardi, G., Pettinau, R., Sainas, F.: Towards benchmarking of solidity verification tools. In: Formal Methods in Blockchain (FMBC). OASIcs, vol.\u00a0118, pp. 6:1\u20136:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/OASICS.FMBC.2024.6","DOI":"10.4230\/OASICS.FMBC.2024.6"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Lande, S., Murgia, M., Zunino, R.: Verifying liquidity of recursive bitcoin contracts. Log. Methods Comput. Sci. 18(1) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(1:22)2022","DOI":"10.46298\/LMCS-18(1:22)2022"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Chaliasos, S., et al.: Smart contract and DeFi security: insights from tool evaluations and practitioner surveys. In: IEEE\/ACM International Conference on Software Engineering (ICSE), pp. 60:1\u201360:13. ACM (2024). https:\/\/doi.org\/10.1145\/3597503.3623302","DOI":"10.1145\/3597503.3623302"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"14_CR16","unstructured":"Defillama. https:\/\/defillama.com\/. Accessed 9 Apr 2024"},{"key":"14_CR17","unstructured":"EIP-4758: Deactivate SELFDESTRUCT. https:\/\/eips.ethereum.org\/EIPS\/eip-4758. Accessed 15 June 2024"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Feist, J., Grieco, G., Groce, A.: Slither: a static analysis framework for smart contracts. In: Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB@ICSE), pp. 8\u201315 (2019). https:\/\/doi.org\/10.1109\/WETSEB.2019.00008","DOI":"10.1109\/WETSEB.2019.00008"},{"issue":"10","key":"14_CR19","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/3416262","volume":"63","author":"N Grech","year":"2020","unstructured":"Grech, N., Kong, M., Jurisevic, A., Brent, L., Scholz, B., Smaragdakis, Y.: MadMax: analyzing the out-of-gas world of smart contracts. Commun. ACM 63(10), 87\u201395 (2020). https:\/\/doi.org\/10.1145\/3416262","journal-title":"Commun. ACM"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-41600-3_11","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"\u00c1 Hajdu","year":"2020","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 161\u2013179. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Hozzov\u00e1, P., Bend\u00edk, J., Nutz, A., Rodeh, Y.: Overapproximation of non-linear integer arithmetic for smart contract verification. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a094, pp. 257\u2013269 (2023). https:\/\/doi.org\/10.29007\/h4p7","DOI":"10.29007\/h4p7"},{"key":"14_CR22","unstructured":"Jackson, D., Nandi, C., Sagiv, M.: Certora technology white paper (2022). https:\/\/docs.certora.com\/en\/latest\/docs\/whitepaper\/index.html"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: Network and Distributed System Security Symposium (NDSS). The Internet Society (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"14_CR24","unstructured":"Kirstein, U.: Formal verification helps finding insolvency bugs - balancer V2 bug report. https:\/\/medium.com\/certora\/formal-verification-helps-finding-insolvency-bugs-balancer-v2-bug-report-1f53ee7dd4d0. Accessed 30 Aug 2024"},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"57037","DOI":"10.1109\/ACCESS.2022.3169902","volume":"10","author":"SS Kushwaha","year":"2022","unstructured":"Kushwaha, S.S., Joshi, S., Singh, D., Kaur, M., Lee, H.N.: Ethereum smart contract analysis tools: a systematic review. IEEE Access 10, 57037\u201357062 (2022). https:\/\/doi.org\/10.1109\/ACCESS.2022.3169902","journal-title":"IEEE Access"},{"key":"14_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2023.100889","volume":"135","author":"C Laneve","year":"2023","unstructured":"Laneve, C.: Liquidity analysis in resource-aware programming. J. Log. Algebraic Methods Program. 135, 100889 (2023). https:\/\/doi.org\/10.1016\/J.JLAMP.2023.100889","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"4","key":"14_CR27","doi-asserted-by":"publisher","first-page":"3110","DOI":"10.1109\/TDSC.2022.3200840","volume":"20","author":"K Nelaturu","year":"2023","unstructured":"Nelaturu, K., Mavridou, A., Stachtiari, E., Veneris, A.G., Laszka, A.: Correct-by-design interacting smart contracts and a systematic approach for verifying ERC20 and ERC721 contracts with VeriSolid. IEEE Trans. Dependable Secur. Comput. 20(4), 3110\u20133127 (2023). https:\/\/doi.org\/10.1109\/TDSC.2022.3200840","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Nguyen, T.D., Pham, L.H., Sun, J., Lin, Y., Minh, Q.T.: sFuzz: an efficient adaptive fuzzer for solidity smart contracts. In: International Conference on Software Engineering (ICSE), pp. 778\u2013788. ACM (2020). https:\/\/doi.org\/10.1145\/3377811.3380334","DOI":"10.1145\/3377811.3380334"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Annual Computer Security Applications Conference (ACSAC), pp. 653\u2013663. ACM (2018). https:\/\/doi.org\/10.1145\/3274694.3274743","DOI":"10.1145\/3274694.3274743"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Permenev, A., Dimitrov, D.K., Tsankov, P., Drachsler-Cohen, D., Vechev, M.T.: VerX: safety verification of smart contracts. In: IEEE Symposium on Security and Privacy, pp. 1661\u20131677. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00024","DOI":"10.1109\/SP40000.2020.00024"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Schiffl, J., Beckert, B.: A practical notion of liveness in smart contract applications. In: Formal Methods in Blockchain (FMBC). OASIcs, vol.\u00a0118, pp. 8:1\u20138:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/OASICS.FMBC.2024.8","DOI":"10.4230\/OASICS.FMBC.2024.8"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Sendner, C., Petzi, L., Stang, J., Dmitrienko, A.: Large-scale study of vulnerability scanners for Ethereum smart contracts. In: IEEE European Symposium on Security and Privacy (S &P), pp. 220\u2013220. IEEE (2024). https:\/\/doi.org\/10.1109\/SP54263.2024.00230","DOI":"10.1109\/SP54263.2024.00230"},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Stephens, J., Ferles, K., Mariano, B., Lahiri, S.K., Dillig, I.: SmartPulse: automated checking of temporal properties in smart contracts. In: IEEE Symposium on Security and Privacy, pp. 555\u2013571. IEEE (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00085","DOI":"10.1109\/SP40001.2021.00085"},{"key":"14_CR34","doi-asserted-by":"publisher","unstructured":"Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., Alexandrov, Y.: SmartCheck: static analysis of Ethereum smart contracts. In: Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pp. 9\u201316. ACM (2018). https:\/\/doi.org\/10.1145\/3194113.3194115","DOI":"10.1145\/3194113.3194115"},{"key":"14_CR35","doi-asserted-by":"publisher","unstructured":"Torres, C.F., Iannillo, A.K., Gervais, A., State, R.: ConFuzzius: a data dependency-aware hybrid fuzzer for smart contracts. In: IEEE European Symposium on Security and Privacy (EuroS &P), pp. 103\u2013119. IEEE (2021). https:\/\/doi.org\/10.1109\/EUROSP51992.2021.00018","DOI":"10.1109\/EUROSP51992.2021.00018"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 67\u201382. ACM (2018). https:\/\/doi.org\/10.1145\/3243734.3243780","DOI":"10.1145\/3243734.3243780"},{"key":"14_CR37","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"},{"key":"14_CR38","doi-asserted-by":"publisher","unstructured":"Xia, P., et al.: Trade or trick?: Detecting and characterizing scam tokens on Uniswap decentralized exchange. In: ACM SIGMETRICS\/IFIP Performance, pp. 23\u201324. ACM (2022). https:\/\/doi.org\/10.1145\/3489048.3522636","DOI":"10.1145\/3489048.3522636"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:29Z","timestamp":1737200309000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}