{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:54Z","timestamp":1780994694647,"version":"3.54.1"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>We describe our experience of using property-based testing---an approach for  \nautomatically generating random inputs to check executable program  \nspecifications---in a development of a higher-order smart contract language that  \npowers a state-of-the-art blockchain with thousands of active daily users.<\/jats:p>\n          <jats:p>We outline the process of integrating QuickChick---a framework for  \nproperty-based testing built on top of the Coq proof assistant---into a  \nreal-world language implementation in OCaml. We discuss the challenges we have  \nencountered when generating well-typed programs for a realistic higher-order  \nsmart contract language, which mixes purely functional and imperative  \ncomputations and features runtime resource accounting. We describe the set of  \nthe language implementation properties that we tested, as well as the semantic  \nharness required to enable their validation. The properties range from the  \nstandard type safety to the soundness of a control- and type-flow analysis used  \nby the optimizing compiler. Finally, we present the list of bugs discovered and  \nrediscovered with the help of QuickChick and discuss their severity and possible  \nramifications.<\/jats:p>","DOI":"10.1145\/3547653","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"886-901","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Random testing of a higher-order blockchain language (experience report)"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7933-4411","authenticated-orcid":false,"given":"Tram","family":"Hoang","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0719-4744","authenticated-orcid":false,"given":"Anton","family":"Trunov","sequence":"additional","affiliation":[{"name":"Zilliqa Research, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0269-9815","authenticated-orcid":false,"given":"Leonidas","family":"Lampropoulos","sequence":"additional","affiliation":[{"name":"University of Maryland at College Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Move: A Language With Programmable Resources.","author":"Blackshear Sam","year":"2019","unstructured":"Sam Blackshear , Evan Cheng , David L. Dill , Victor Gao , Ben Maurer , Todd Nowacki , Alistair Pott , Shaz Qadeer , Rain, Dario Russi , Stephane Sezer , Tim Zakian , and Runtian Zhou . 2019 . Move: A Language With Programmable Resources. Available at https:\/\/developers.diem.com\/papers\/diem-move-a-language-with-programmable-resources\/2019-06-18.pdf Sam Blackshear, Evan Cheng, David L. Dill, Victor Gao, Ben Maurer, Todd Nowacki, Alistair Pott, Shaz Qadeer, Rain, Dario Russi, Stephane Sezer, Tim Zakian, and Runtian Zhou. 2019. Move: A Language With Programmable Resources. Available at https:\/\/developers.diem.com\/papers\/diem-move-a-language-with-programmable-resources\/2019-06-18.pdf"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00084"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_4_1","unstructured":"Guillaume Claret. 2021. Coq-of-OCaml A Compiler from OCaml to Coq. Available at https:\/\/formal.land\/docs\/coq-of-ocaml\/introduction \t\t\t\t  Guillaume Claret. 2021. Coq-of-OCaml A Compiler from OCaml to Coq. Available at https:\/\/formal.land\/docs\/coq-of-ocaml\/introduction"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.150"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"e_1_2_1_8_1","unstructured":"Ethereum Foundation. 2018. ERC20 Token Standard. https:\/\/en.bitcoinwiki.org\/wiki\/ERC20 Online \t\t\t\t  Ethereum Foundation. 2018. ERC20 Token Standard. https:\/\/en.bitcoinwiki.org\/wiki\/ERC20 Online"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41582-1_8"},{"key":"e_1_2_1_11_1","volume-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 de Paris VII","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard . 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 de Paris VII . Paris, France . Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 de Paris VII. Paris, France."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_10"},{"key":"e_1_2_1_13_1","unstructured":"Emin G\u00fcn Sirer. 2016. Reentrancy Woes in Smart Contracts. http:\/\/hackingdistributed.com\/2016\/07\/13\/reentrancy-woes\/ \t\t\t\t  Emin G\u00fcn Sirer. 2016. Reentrancy Woes in Smart Contracts. http:\/\/hackingdistributed.com\/2016\/07\/13\/reentrancy-woes\/"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6610599"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000058"},{"key":"e_1_2_1_17_1","volume-title":"Plutus: A Functional Contract Platform. https:\/\/testnet.iohkdev.io\/en\/plutus\/ Online","author":"Foundation IOHK","year":"2019","unstructured":"IOHK Foundation . 2019 . Plutus: A Functional Contract Platform. https:\/\/testnet.iohkdev.io\/en\/plutus\/ Online ; accessed 23 February 2022 IOHK Foundation. 2019. Plutus: A Functional Contract Platform. https:\/\/testnet.iohkdev.io\/en\/plutus\/ Online; accessed 23 February 2022"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330553"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_20_1","volume-title":"Random Testing for Language Design. Ph. D. Dissertation","author":"Lampropoulos Leonidas","unstructured":"Leonidas Lampropoulos . 2018. Random Testing for Language Design. Ph. D. Dissertation . University of Pennsylvania . Leonidas Lampropoulos. 2018. Random Testing for Language Design. Ph. D. Dissertation. University of Pennsylvania."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_1_23_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018","unstructured":"Leonidas Lampropoulos and Benjamin C . Pierce . 2018 . QuickChick: Property- Based Testing In Coq. Software Foundations series, Volume 4 . Electronic textbook. https:\/\/softwarefoundations.cis.upenn.edu\/ Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickChick: Property-Based Testing In Coq. Software Foundations series, Volume 4. Electronic textbook. https:\/\/softwarefoundations.cis.upenn.edu\/"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092711"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213847"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110259"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2015.7102603"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_25"},{"key":"e_1_2_1_30_1","volume-title":"Compiling a Higher-Order Smart Contract Language to LLVM. CoRR, abs\/2008.05555","author":"Nagaraj Vaivaswatha","year":"2020","unstructured":"Vaivaswatha Nagaraj , Jacob Johannsen , Anton Trunov , George P\u00eerlea , Amrit Kumar , and Ilya Sergey . 2020. Compiling a Higher-Order Smart Contract Language to LLVM. CoRR, abs\/2008.05555 ( 2020 ), arxiv:2008.05555 Vaivaswatha Nagaraj, Jacob Johannsen, Anton Trunov, George P\u00eerlea, Amrit Kumar, and Ilya Sergey. 2020. Compiling a Higher-Order Smart Contract Language to LLVM. CoRR, abs\/2008.05555 (2020), arxiv:2008.05555"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_2_1_33_1","volume-title":"Broken Metre: Attacking Resource Metering in EVM","author":"Perez Daniel","year":"2020","unstructured":"Daniel Perez and Benjamin Livshits . 2020 . Broken Metre: Attacking Resource Metering in EVM . In NDSS. The Internet Society . Daniel Perez and Benjamin Livshits. 2020. Broken Metre: Attacking Resource Metering in EVM. In NDSS. The Internet Society."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454112"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"e_1_2_1_36_1","volume-title":"Writing Safe Smart Contracts in Flint. Master\u2019s thesis","author":"Schrans Franklin","unstructured":"Franklin Schrans . 2018. Writing Safe Smart Contracts in Flint. Master\u2019s thesis . Imperial College London . Franklin Schrans. 2018. Writing Safe Smart Contracts in Flint. Master\u2019s thesis. Imperial College London."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"e_1_2_1_39_1","volume-title":"Control-Flow Analysis of Higher-Order Languages or Taming Lambda. Ph. D. Dissertation. School of Computer Science","author":"Shivers Olin","unstructured":"Olin Shivers . 1991. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. Ph. D. Dissertation. School of Computer Science , Carnegie Mellon University . Olin Shivers. 1991. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. Ph. D. Dissertation. School of Computer Science, Carnegie Mellon University."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_2_1_41_1","volume-title":"Michelson: the language of Smart Contracts in Tezos. https:\/\/tezos.gitlab.io\/whitedoc\/michelson.html Online","author":"Foundation Tezos","year":"2022","unstructured":"Tezos Foundation . 2018. Michelson: the language of Smart Contracts in Tezos. https:\/\/tezos.gitlab.io\/whitedoc\/michelson.html Online ; accessed 23 February 2022 Tezos Foundation. 2018. Michelson: the language of Smart Contracts in Tezos. https:\/\/tezos.gitlab.io\/whitedoc\/michelson.html Online; accessed 23 February 2022"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159877"},{"key":"e_1_2_1_43_1","volume-title":"Ethereum: A Secure Decentralized Generalised Transaction Ledger.","author":"Wood Gavin","year":"2014","unstructured":"Gavin Wood . 2014 . Ethereum: A Secure Decentralized Generalised Transaction Ledger. Gavin Wood. 2014. Ethereum: A Secure Decentralized Generalised Transaction Ledger."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547653","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547653","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547653"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":44,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547653"],"URL":"https:\/\/doi.org\/10.1145\/3547653","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}