{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:27:49Z","timestamp":1769725669454,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats: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\u2019s 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\u2019s 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.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_16","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"325-338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["SolCMC: Solidity Compiler\u2019s Model Checker"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"Alt","sequence":"first","affiliation":[]},{"given":"Martin","family":"Blicha","sequence":"additional","affiliation":[]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"16_CR1","unstructured":"Act 0.1 released. https:\/\/fv.ethereum.org\/2021\/08\/31\/act-0.1\/. Accessed 21 Feb 2022"},{"key":"16_CR2","unstructured":"Deposit Contract deployed on Ethereum mainnet. https:\/\/etherscan.io\/address\/0x00000000219ab540356cbb839cbe05303d7705fa#code. Accessed 21 Jan 2022"},{"key":"16_CR3","unstructured":"Deposit Contract specification and source code. https:\/\/github.com\/ethereum\/consensus-specs\/blob\/master\/specs\/phase0\/deposit-contract.md. Accessed 21 Jan 2022"},{"key":"16_CR4","unstructured":"Echidna source code and documentation. https:\/\/github.com\/crytic\/echidna\/, Accessed 21 Jan 2022"},{"key":"16_CR5","unstructured":"ERC20 documentation. https:\/\/eips.ethereum.org\/EIPS\/eip-20. Accessed 21 Jan 2022"},{"key":"16_CR6","unstructured":"ERC777 documentation. https:\/\/eips.ethereum.org\/EIPS\/eip-777. Accessed 21 Jan 2022"},{"key":"16_CR7","unstructured":"ERC777 Property Wrapper contract. https:\/\/github.com\/leonardoalt\/openzeppelin-contracts\/blob\/master\/contracts\/token\/ERC777\/ERC777PropertyUnsafe.sol. Accessed 21 Jan 2022"},{"key":"16_CR8","unstructured":"ERC777 using a mutex to prevent reentrancy. https:\/\/github.com\/leonardoalt\/openzeppelin-contracts\/blob\/master\/contracts\/token\/ERC777\/ERC777Mutex.sol. Accessed 21 Jan 2022"},{"key":"16_CR9","unstructured":"Ethereum Consensus Layer specification. https:\/\/github.com\/ethereum\/consensus-specs. Accessed 21 Jan 2022"},{"key":"16_CR10","unstructured":"K framework. https:\/\/kframework.org. Accessed 21 Jan 2022"},{"key":"16_CR11","unstructured":"Openzeppelin Solidity implementation of the ERC777 standard. https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts\/blob\/master\/contracts\/token\/ERC777\/ERC777.sol. Accessed 21 Jan 2022"},{"key":"16_CR12","unstructured":"Remix IDE. https:\/\/remix.ethereum.org. Accessed 21 Jan 2022"},{"key":"16_CR13","unstructured":"Scribble documentation. https:\/\/docs.scribble.codes\/language\/introduction. Accessed 21 Jan 2022"},{"key":"16_CR14","unstructured":"Slither source code and documentation. https:\/\/github.com\/crytic\/slither. Accessed 21 Jan 2022"},{"key":"16_CR15","unstructured":"solc-js documentation. https:\/\/github.com\/ethereum\/solc-js. Accessed 21 Jan 2022"},{"key":"16_CR16","unstructured":"SolCMC documentation. https:\/\/docs.soliditylang.org\/en\/latest\/smtchecker.html. Accessed 21 Jan 2022"},{"key":"16_CR17","unstructured":"SolCMC tests. https:\/\/github.com\/ethereum\/solidity\/tree\/develop\/test\/libsolidity\/smtCheckerTests. Accessed 21 Jan 2022"},{"key":"16_CR18","unstructured":"SolCMC tests\u2019 Horn queries. https:\/\/github.com\/leonardoalt\/chc_benchmarks_solidity. Accessed 21 Jan 2022"},{"key":"16_CR19","unstructured":"Solidity compiler input and output JSON description. https:\/\/docs.soliditylang.org\/en\/v0.8.11\/using-the-compiler.html#compiler-input-and-output-json-description. Accessed 21 Jan 2022"},{"key":"16_CR20","unstructured":"Solidity NatSpec Format. https:\/\/docs.soliditylang.org\/en\/v0.8.11\/natspec-format.html. Accessed 21 Jan 2022"},{"key":"16_CR21","unstructured":"Solidity\u2019s SMT callback documentation. https:\/\/github.com\/ethereum\/solc-js#example-usage-with-smtsolver-callback. Accessed 21 Jan 2022"},{"key":"16_CR22","unstructured":"Symbolic execution for hevm. https:\/\/fv.ethereum.org\/2020\/07\/28\/symbolic-hevm-release\/. Accessed 21 Jan 2022"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"16_CR24","unstructured":"Bernardi, T.P., et al.: WIP: finding bugs automatically in smart contracts with parameterized invariants (2020). https:\/\/www.certora.com\/pubs\/sbc2020.pdf. Accessed 21 Jan 2022"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-18170-9_151","volume-title":"Computation Theory and Logic","author":"A Blass","year":"1987","unstructured":"Blass, A., Gurevich, Y.: Existential fixed-point logic. In: B\u00f6rger, E. (ed.) Computation Theory and Logic. LNCS, vol. 270, pp. 20\u201336. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18170-9_151"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-030-90870-6_24","volume-title":"Formal Methods","author":"F Cassez","year":"2021","unstructured":"Cassez, F.: Verification of the Incremental Merkle Tree Algorithm with Dafny. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 445\u2013462. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_24"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-41600-3_11","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"\u00c1 Hajdu","year":"2020","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 161\u2013179. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the ethereum virtual machine. In: Proceedings of CSF 2018, pp. 204\u2013217. IEEE Computer Society (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA Horn solver. In: Proceedings FMCAD 2018, pp. 1\u20137. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"issue":"3","key":"16_CR31","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods in System Design 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods in System Design"},{"key":"16_CR32","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-662-50497-0_4","volume-title":"Decision Procedures","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Equality Logic and Uninterpreted Functions. In: Decision Procedures. TTCSAES, pp. 77\u201395. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-50497-0_4"},{"key":"16_CR33","unstructured":"Leino, K.R.M.: This is Boogie 2, June 2008. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"16_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-030-61467-6_12","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"M Marescotti","year":"2020","unstructured":"Marescotti, M., Otoni, R., Alt, L., Eugster, P., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Accurate smart contract verification through direct modelling. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 178\u2013194. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_12"},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Z3: An efficient SMT solver (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-53288-8_8","volume-title":"Computer Aided Verification","author":"D Park","year":"2020","unstructured":"Park, D., Zhang, Y., Rosu, G.: End-to-end formal verification of\u00a0ethereum 2.0 deposit smart contract. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 151\u2013164. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_8"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Schneidewind, C., Grishchenko, I., Scherer, M., Maffei, M.: EThor: practical and provably sound static analysis of ethereum smart contracts, pp. 621\u2013640. ACM (2020)","DOI":"10.1145\/3372297.3417250"},{"key":"16_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-030-41600-3_7","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"Y Wang","year":"2020","unstructured":"Wang, Y., Lahiri, S.K., Chen, S., Pan, R., Dillig, I., Born, C., Naseer, I., Ferles, K.: Formal verification of workflow policies for smart contracts in azure blockchain. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 87\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_7"},{"key":"16_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-030-94583-1_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Wesley","year":"2022","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R., W\u00fcstholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstraction in SmartACE. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 425\u2013449. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:13:45Z","timestamp":1667495625000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}