6 papers
LLMs as verification oracles for Solidity
Massimo Bartoletti, Enrico Lipparini, Livio Pompianu
Ensuring the correctness of smart contracts is critical, as even subtle flaws can lead to severe financial losses. While bug detection tools able to spot common vulnerability patte…
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Enrico Lipparini, Thomas Hader, Ahmed Irfan +1
The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by increm…
A theory of Lending Protocols in DeFi
Massimo Bartoletti, Enrico Lipparini
Lending protocols are one of the main applications of Decentralized Finance (DeFi), enabling crypto-assets loan markets with a total value estimated in the tens of billions of doll…
Formal verification in Solidity and Move: insights from a comparative analysis
Massimo Bartoletti, Silvia Crafa, Enrico Lipparini
Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is c…
Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
Enrico Lipparini, Stefan Ratschan
For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satis…
Solvent: liquidity verification of smart contracts
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini +1
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…