@conference {369,
	title = {SolCMC: Solidity Compiler{\textquoteright}s Model Checker},
	booktitle = {CAV},
	year = {2022},
	address = { Haifa, Isreal},
	abstract = {<p>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{\textquoteright}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{\textquoteright}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.</p>
},
	keywords = {SolCMC},
	author = {Leonardo Alt and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
@article {373,
	title = {A Solicitous Approach to Smart Contract Verification},
	journal = {ACM Transactions on Privacy and Security},
	year = {2022},
	type = {Full-Length Research Paper},
	url = {https://dl.acm.org/doi/10.1145/3564699},
	author = {Rodrigo Otoni and Matteo Marescotti and Leonardo Alt and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
}
