Automated construction of predicate abstractions for smart contract validation
File(s)
Accepted version
Author(s)
Godoy, Javier
Torres, Eden
Galeotti, Juan P
Garbervetsky, Diego
Uchitel, Sebastian
Type
Journal Article
Abstract
Verification and validation of smart contracts is crucial, as these programs administer valuable assets. Indeed, there is a proliferation of companies, specialized in smart contract audits that has become a key component of the blockchain ecosystem. Current verification and validation practice is heavily reliant on the insight and experience of auditors. However, there is an increasing rich toolbox that supports their work. In this paper, we show how predicate abstraction can be leveraged to construct models that support smart contract auditing. These models provide auditors with a systematic approach to analyzing and validating the behavior of smart contracts at the function call level. By proposing predicates, auditors can generate alternative perspectives on a contract’s behavior, refine transitions to investigate specific scenarios, and incorporate transient states into the abstraction to uncover reentrancy vulnerabilities. We formally define predicate abstractions for smart contracts and introduce default predicates to support initial exploration. We also present PASCo, a tool that automatically builds an abstract finite state automaton from a set of predicates and a smart contract implementation. We evaluate PASCo on established benchmarks and with an experienced smart contract auditor. Furthermore, we compare its effectiveness in detecting reentrancy vulnerabilities (measured in terms of precision and recall) against 14 state-of-the-art Solidity vulnerability detectors.
Date Issued
2025-10-27
Date Acceptance
2025-09-24
Citation
Software and Systems Modeling (SoSyM), 2025
ISSN
1619-1366
Publisher
Springer
Journal / Book Title
Software and Systems Modeling (SoSyM)
Copyright Statement
Copyright © The Author(s), under exclusive licence to Springer-Verlag GmbH Germany, part of Springer Nature 2025. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Subjects
Computer Science
Computer Science, Software Engineering
Predicate abstraction
Science & Technology
Smart contracts
Software validation
Technology
Publication Status
Unpublished
Date Publish Online
2025-10-27