2024/04/27 by Massimo Bartoletti, Angelo Ferrando, Bartoletti, Massimo +5 · 1 citation
Economics, Econometrics and Finance · #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Insurance and Financial Risk Management #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2404.17864
openalex publication_date 2024/04/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts.