SolCMC: Solidity Compiler’s Model Checker

Title:

SolCMC: Solidity Compiler’s Model Checker

Authors:

L. Alt, M. Blicha, A. Hyvärinen, N. Sharygina

Publication:

Computer Aided Verification

DOI:

Year:

2022

ISBN:

978-3-031-13185-1

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.

BibTeX:

@inproceedings{alt_solcmc_2022,
    title = {{SolCMC: Solidity Compiler’ s Model Checker}},
    author = {Alt, Leonardo and Blicha, Martin and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2022},
    booktitle = {{Computer Aided Verification}},
    editor = {Shoham, Sharon and Vizel, Yakir},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-031-13185-1_16},
    isbn = {978-3-031-13185-1},
    pages = {325--338},
    shorttitle = {SolCMC},
}