Skip to main content
Conference ProceedingsOPEN ACCESS

SolCMC: Solidity Compiler’s Model Checker

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2022) 13371 LNCS 325-338
DOI: 10.1007/978-3-031-13185-1_16
15Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation’s Solidity compiler ships with a model checker. The checker, called SolCMC, has two different reasoning engines and tracks closely the development of the Solidity language. We describe SolCMC’s architecture and use from the perspective of developers of both smart contracts and tools for software verification, and show how to analyze nontrivial properties of real life contracts in a fully automated manner.

Author supplied keywords

Cite

CITATION STYLE

APA

Alt, L., Blicha, M., Hyvärinen, A. E. J., & Sharygina, N. (2022). SolCMC: Solidity Compiler’s Model Checker. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13371 LNCS, pp. 325–338). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-13185-1_16

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free