{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:37:54Z","timestamp":1742963874445,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720124"},{"type":"electronic","value":"9783030720131"}],"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,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"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>A <jats:italic>smart contract<\/jats:italic> is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them.<\/jats:p><jats:p>This tool paper describes our type-based static verification tool <jats:sc>Helmholtz<\/jats:sc> for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. <jats:sc>Helmholtz<\/jats:sc> is designed on top of our extension of Michelson\u2019s type system with refinement types. <jats:sc>Helmholtz<\/jats:sc> takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. <jats:sc>Helmholtz<\/jats:sc> successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_14","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"262-280","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5941-6770","authenticated-orcid":false,"given":"Yuki","family":"Nishida","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiromasa","family":"Saito","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ran","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akira","family":"Kawata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Furuse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-8789","authenticated-orcid":false,"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"14_CR1","unstructured":"Michelson: the language of smart contracts in Tezos. https:\/\/tezos.gitlab.io\/whitedoc\/michelson.html, retrieved Oct. 14, 2020."},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Benton, N.: A Typed, Compositional Logic for a Stack-Based Abstract Machine. In: Proceedings of Asian Sympoisum on Programming Languages and Systems (APLAS). pp. 364\u2013380. Springer Berlin Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_24","DOI":"10.1007\/11575467_24"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In: Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I. Lecture Notes in Computer Science, vol. 12232, pp. 368\u2013379. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_28","DOI":"10.1007\/978-3-030-54994-7_28"},{"key":"14_CR4","unstructured":"Goodman, L.: Tezos \u2014 a self-amending crypto-ledger. white paper. https:\/\/tezos.com\/static\/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf (2014), retrieved Oct. 14, 2020."},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Grossman, S., Abraham, I., Golan-Gueta, G., Michalevsky, Y., Rinetzky, N., Sagiv, M., Zohar, Y.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2(POPL) (Dec 2017). https:\/\/doi.org\/10.1145\/3158136","DOI":"10.1145\/3158136"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). pp. 204\u2013217 (Jul 2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Financial Cryptography and Data Security. pp. 520\u2013535. Springer International Publishing (2017)","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N.: A compositional logic for polymorphic higher-order functions. In: Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 24-26 August 2004, Verona, Italy. pp. 191\u2013202. ACM (2004). https:\/\/doi.org\/10.1145\/1013963.1013985","DOI":"10.1145\/1013963.1013985"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Kawaguchi, M., Rondon, P.M., Jhala, R.: Type-based data structure verification. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009. pp. 304\u2013315. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542510","DOI":"10.1145\/1542476.1542510"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011,San Jose, CA, USA, June 4-8, 2011. pp. 222\u2013233 (2011). https:\/\/doi.org\/10.1145\/1993498.1993525","DOI":"10.1145\/1993498.1993525"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"14_CR12","unstructured":"Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system. https:\/\/bitcoin.org\/bitcoin.pdf (2008), retrieved Oct. 12, 2020."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Owens, S., B\u00f6hm, P., Zappa\u00a0Nardelli, F., Sewell, P.: Lem: A lightweight tool for heavyweight semantics. In: Interactive Theorem Proving. pp. 363\u2013369. Springer Berlin Heidelberg (2011)","DOI":"10.1007\/978-3-642-22863-6_27"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Ro\u015fu, G.: A formal verification tool for Ethereum VM bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. pp. 912\u2013915. ACM (Oct 2018). https:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"14_CR15","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press (2002)"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. pp. 159\u2013169 (2008). https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Ro\u015fu, G., \u015eerb\u0103nut\u0103, T.F.: An overview of the K semantic framework. The Journal of Logic and Algebraic Programming 79(6), 397\u2013434 ( 2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"14_CR18","unstructured":"Siegel, D.: Understanding the DAO attack. CoinDesk (2016), https:\/\/www.coindesk.com\/understanding-dao-hack-journalists, retrieved Oct. 13, 2020."},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (Sep 1997). https:\/\/doi.org\/10.5210\/fm.v2i9.548","DOI":"10.5210\/fm.v2i9.548"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. pp. 119\u2013130 (2010). https:\/\/doi.org\/10.1145\/1706299.1706315","DOI":"10.1145\/1706299.1706315"},{"key":"14_CR21","unstructured":"The Coq development team: The coq proof assistant reference manual (2020), http:\/\/coq.inria.fr, version 8.12.0"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal. pp. 277\u2013288 (2009). https:\/\/doi.org\/10.1145\/1599410.1599445","DOI":"10.1145\/1599410.1599445"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Jones, S.L.P.: Refinement types for Haskell. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. pp. 269\u2013282. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Xi, H.: Dependent ML an approach to practical programming with dependent types. J. Funct. Program. 17(2), 215\u2013286 (2007). https:\/\/doi.org\/10.1017\/S0956796806006216","DOI":"10.1017\/S0956796806006216"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Xi, H., Harper, R.: A dependently typed assembly language. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201901), Firenze (Florence), Italy, September 3-5, 2001. pp. 169\u2013180. ACM (2001). https:\/\/doi.org\/10.1145\/507635.507657","DOI":"10.1145\/507635.507657"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. pp. 295\u2013314 (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_19","DOI":"10.1007\/978-3-642-35873-9_19"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:14:19Z","timestamp":1616436859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_14","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":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"141","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":"41","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":"21","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":"29% - 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":"The conference changed to an online format due to the COVID-19 pandemic","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)"}}]}}