{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T01:13:00Z","timestamp":1782522780750,"version":"3.54.5"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,5,27]],"date-time":"2022-05-27T00:00:00Z","timestamp":1653609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,5,27]],"date-time":"2022-05-27T00:00:00Z","timestamp":1653609600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"tezos foundations"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["New Gener. Comput."],"published-print":{"date-parts":[[2022,7]]},"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. This article 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\/s00354-022-00167-1","type":"journal-article","created":{"date-parts":[[2022,5,27]],"date-time":"2022-05-27T07:07:37Z","timestamp":1653635257000},"page":"507-540","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types"],"prefix":"10.1007","volume":"40","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5941-6770","authenticated-orcid":false,"given":"Yuki","family":"Nishida","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hiromasa","family":"Saito","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ran","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Akira","family":"Kawata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jun","family":"Furuse","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7466-8789","authenticated-orcid":false,"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,5,27]]},"reference":[{"key":"167_CR1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031","author":"J Bengtson","year":"2011","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. (2011). https:\/\/doi.org\/10.1145\/1890028.1890031","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"167_CR2","doi-asserted-by":"publisher","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Proceedings of Asian Symposium on Programming Languages and Systems (APLAS), pp. 364\u2013380. Springer, Berlin (2005). https:\/\/doi.org\/10.1007\/11575467_24","DOI":"10.1007\/11575467_24"},{"key":"167_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\u2014Porto, Portugal, October 7\u201311, 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":"167_CR4","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\u2013April 6, 2008. Proceedings, pp. 337\u2013340 (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"167_CR5","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"2001","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (2001)"},{"key":"167_CR6","unstructured":"Goodman, L.: Tezos\u2014a self-amending crypto-ledger. white paper (2014). https:\/\/tezos.com\/static\/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf. Accessed 14 Oct 2020"},{"key":"167_CR7","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. In: Proc. ACM Program. Lang., vol. 2 (POPL) (2017). https:\/\/doi.org\/10.1145\/3158136","DOI":"10.1145\/3158136"},{"key":"167_CR8","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 (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"167_CR9","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":"167_CR10","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\u201326 August 2004, Verona, Italy, pp. 191\u2013202. ACM (2004). https:\/\/doi.org\/10.1145\/1013963.1013985","DOI":"10.1145\/1013963.1013985"},{"key":"167_CR11","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\u201321, 2009, pp. 304\u2013315. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542510","DOI":"10.1145\/1542476.1542510"},{"key":"167_CR12","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\u20138, 2011, pp. 222\u2013233 (2011). \nhttps:\/\/doi.org\/10.1145\/1993498.1993525","DOI":"10.1145\/1993498.1993525"},{"key":"167_CR13","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https:\/\/bitcoin.org\/bitcoin.pdf. Accessed 12 Oct 2020"},{"key":"167_CR14","unstructured":"Nomadic Labs.: Michelson: the language of smart contracts in Tezos. https:\/\/tezos.gitlab.io\/whitedoc\/michelson.html. Accessed 14 Oct 2020"},{"key":"167_CR15","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 (2011)","DOI":"10.1007\/978-3-642-22863-6_27"},{"key":"167_CR16","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 (2018).  https:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"167_CR17","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\u201313, 2008, pp. 159\u2013169 (2008). \nhttps:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"issue":"6","key":"167_CR18","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nut\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","journal-title":"J. Logic Algebraic Program."},{"key":"167_CR19","unstructured":"Siegel, D.: Understanding the DAO attack. CoinDesk (2016). https:\/\/www.coindesk.com\/understanding-dao-hack-journalists. Accessed 13 Oct 2020"},{"key":"167_CR20","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548","author":"N Szabo","year":"1997","unstructured":"Szabo, N.: Formalizing and securing relationships on public networks. First Monday (1997). https:\/\/doi.org\/10.5210\/fm.v2i9.548","journal-title":"First Monday"},{"key":"167_CR21","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\u201323, 2010, pp. 119\u2013130 (2010). https:\/\/doi.org\/10.1145\/1706299.1706315","DOI":"10.1145\/1706299.1706315"},{"key":"167_CR22","unstructured":"The Coq development team.: The coq proof assistant reference manual. Version 8.12.0 (2020). http:\/\/coq.inria.fr"},{"key":"167_CR23","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\u20139, 2009, Coimbra, Portugal, pp. 277\u2013288 (2009). https:\/\/doi.org\/10.1145\/1599410.1599445","DOI":"10.1145\/1599410.1599445"},{"key":"167_CR24","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\u20133, 2014, pp. 269\u2013282. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"167_CR25","doi-asserted-by":"publisher","unstructured":"Vazou, N., Tondwalkar, A., Choudhury, V., Scott, R.G., Newton, R.R., Wadler, P., Jhala, R.: Refinement reflection: Complete verification with SMT. In: Proc. ACM Program. Lang., vol. 2 (POPL) (2017). https:\/\/doi.org\/10.1145\/3158141","DOI":"10.1145\/3158141"},{"issue":"2","key":"167_CR26","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1017\/S0956796806006216","volume":"17","author":"H Xi","year":"2007","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","journal-title":"J. Funct. Program."},{"key":"167_CR27","doi-asserted-by":"publisher","unstructured":"Xi, H., Harper, R.: A dependently typed assembly language. In: Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201901), Firenze (Florence), Italy, September 3\u20135, 2001, pp. 169\u2013180. ACM (2001). https:\/\/doi.org\/10.1145\/507635.507657","DOI":"10.1145\/507635.507657"},{"key":"167_CR28","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\u201322, 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":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-022-00167-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00354-022-00167-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00354-022-00167-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T19:42:49Z","timestamp":1662493369000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00354-022-00167-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,27]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,7]]}},"alternative-id":["167"],"URL":"https:\/\/doi.org\/10.1007\/s00354-022-00167-1","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"value":"0288-3635","type":"print"},{"value":"1882-7055","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,27]]},"assertion":[{"value":"1 August 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"No conflicts.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}