{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:18:55Z","timestamp":1742915935145,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Some of the most significant high-level properties of currencies are the sums of certain account balances. Properties of such sums can ensure the integrity of currencies and transactions. For example, the sum of balances should not be changed by a transfer operation. Currencies manipulated by code present a verification challenge to mathematically prove their integrity by reasoning about computer programs that operate over them, e.g., in Solidity. The ability to reason about sums is essential: even the simplest ERC-20 token standard of the Ethereum community provides a way to access the total supply of balances.<\/jats:p><jats:p>Unfortunately, reasoning about code written against this interface is non-trivial: the number of addresses is unbounded, and establishing global invariants like the preservation of the sum of the balances by operations like transfer requires higher-order reasoning. In particular, automated reasoners do not provide ways to specify summations of arbitrary length.<\/jats:p><jats:p>In this paper, we present a generalization of first-order logic which can express the unbounded sum of balances. We prove the decidablity of one of our extensions and the undecidability of a slightly richer one. We introduce first-order encodings to automate reasoning over software transitions with summations. We demonstrate the applicability of our results by using SMT solvers and first-order provers for validating the correctness of common transitions in smart contracts.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_15","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"317-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Summing up Smart Transitions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5503-5791","authenticated-orcid":false,"given":"Neta","family":"Elad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8940-4989","authenticated-orcid":false,"given":"Sophie","family":"Rain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6609-5952","authenticated-orcid":false,"given":"Neil","family":"Immerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0845-5811","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0723-1309","authenticated-orcid":false,"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"15_CR1","unstructured":"SMTLIB: Satisfiability Modulo Theories Library. https:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.6-r2017-07-18.pdf"},{"key":"15_CR2","unstructured":"Certora Ltd: The Certora Verifier (2020). www.certora.com"},{"key":"15_CR3","unstructured":"Concourse Open Community: DeFi Pulse (2020). https:\/\/defipulse.com\/"},{"key":"15_CR4","unstructured":"Alt, L.: Solidity\u2019s SMTChecker can Automatically find Real Bugs (2019). https:\/\/medium.com\/@leonardoalt\/soliditys-smtchecker-can-automatically-find-real-bugs-beb566c24dea"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Reynolds, A., El Ouraoui, D., Tinelli, C., Barrett, C.: Extending SMT solvers to higher-order logic. In: CADE, pp. 35\u201354 (2019)","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., et al.: CVC4. In: CAV, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR8","unstructured":"Denecker, M., De Cat, B.: DPLL (Agg): an efficient SMT module for aggregates. In: Logic and Search (2010)"},{"key":"15_CR9","unstructured":"Dutertre, B., De Moura, L.: The Yices SMT Solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf, pp. 1\u20132 (2006)"},{"key":"15_CR10","unstructured":"Elad, N., Rain, S., Immerman, N., Kov\u00e1cs, L., Sagiv, M.: Summing up smart transitions (2021). https:\/\/arxiv.org\/abs\/2105.07663"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, A.: Modal and temporal logics. In: Handbook of Theoretical Computer Science, vol. B, pp. 995\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Etessami, K.: Counting quantifiers, successor relations, and logarithmic space. In: JCSS, pp. 400\u2013411 (1997)","DOI":"10.1006\/jcss.1997.1485"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Gleiss, B., Suda, M.: Layered clause selection for saturation-based theorem proving. In: IJCAR, pp. 34\u201352 (2020)","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovic, D.: Solc-verify: a modular verifier for solidity smart contracts. In: VSTTE, pp. 161\u2013179 (2019)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Schoisswohl, J., Voronkov, A.: Induction with generalization in superposition reasoning. In: CICM, pp. 123\u2013137 (2020)","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Hella, L., Libkin, L., Nurmonen, J., Wong, L.: Logics with aggregate operators. J. ACM. 48(8), 880\u2013907 (2001)","DOI":"10.1145\/502090.502100"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: FC, pp. 520\u2013535 (2017)","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: NDSS (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: CAV, pp. 1\u201335 (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: CADE, pp. 260\u2013277 (2005)","DOI":"10.1007\/11532231_20"},{"key":"15_CR21","unstructured":"Libkin, L.: Logics with counting, auxiliary relations, and lower bounds for invariant queries. In: LICS, pp. 316\u2013325 (1999)"},{"key":"15_CR22","unstructured":"Nipkow, T.: Interactive proof: introduction to Isabelle\/HOL. In: Software Safety and Security, pp. 254\u2013285 (2012)"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Park, D., Zhang, Y., Rosu, G.: End-to-end formal verification of Ethereum 2.0 deposit smart contract. In: CAV, pp. 151\u2013164 (2020)","DOI":"10.1007\/978-3-030-53288-8_8"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., et al.: The Imandra automated reasoning system (system description). In: IJCAR, pp. 464\u2013471 (2020)","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Passmore, G.O.: Formal verification of financial algorithms with Imandra. In: FMCAD, pp. i\u2013i (2018)","DOI":"10.1007\/978-3-319-63046-5_3"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., Ignatovich, D.: Formal verification of financial algorithms. In: CADE, pp. 26\u201341 (2017)","DOI":"10.1007\/978-3-319-63046-5_3"},{"key":"15_CR27","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I congres de Math\u00e9maticiens des Pays Slaves, pp. 92\u2013101 (1929)"},{"key":"15_CR28","unstructured":"Sadiku, M., Eze, K., Musa, S.: Smart contracts: a primer (2018)"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Schneidewind, C., Grishchenko, I., Scherer, M., Maffei, M.: eThor: practical and provably sound static analysis of Ethereum smart contracts. In: CCS, pp. 621\u2013640 (2020)","DOI":"10.1145\/3372297.3417250"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: SmartPulse: automated checking of temporal properties in smart contracts. In: IEEE S&P (2021)","DOI":"10.1109\/SP40001.2021.00085"},{"key":"15_CR31","unstructured":"V\u00e4\u00e4n\u00e4nen, J.A.: Generalized quantifiers. In: Bull. EATCS (1997)"},{"key":"15_CR32","unstructured":"Vogelsteller, F., Buterin, V.: EIP-20: ERC-20 token standard. In: EIP no. 20 (2015)"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Wang, Y., et al.: Formal verification of workflow policies for smart contracts in azure blockchain. In: VSTTE, pp. 87\u2013106 (2019)","DOI":"10.1007\/978-3-030-41600-3_7"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: CADE, pp. 140\u2013145 (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Zhong, J.E., et al.: The move prover. In: CAV, pp. 137\u2013150 (2020)","DOI":"10.1007\/978-3-030-53288-8_7"}],"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-030-81685-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T10:49:21Z","timestamp":1725446961000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","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":"290","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":"63","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":"0","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":"22% - 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","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":"12","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)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}