SolCMC: Solidity Compiler's Model Checker
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F22%3A10455351" target="_blank" >RIV/00216208:11320/22:10455351 - isvavai.cz</a>
Výsledek na webu
<a href="https://doi.org/10.1007/978-3-031-13185-1_16" target="_blank" >https://doi.org/10.1007/978-3-031-13185-1_16</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-13185-1_16" target="_blank" >10.1007/978-3-031-13185-1_16</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
SolCMC: Solidity Compiler's Model Checker
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
SolCMC: Solidity Compiler's Model Checker
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2022
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
COMPUTER AIDED VERIFICATION (CAV 2022), PT I
ISBN
978-3-031-13184-4
ISSN
0302-9743
e-ISSN
1611-3349
Počet stran výsledku
14
Strana od-do
325-338
Název nakladatele
SPRINGER INTERNATIONAL PUBLISHING AG
Místo vydání
CHAM
Místo konání akce
Haifa
Datum konání akce
7. 8. 2022
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000870304500016