{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:52:48Z","timestamp":1766451168253,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,23]],"date-time":"2022-10-23T00:00:00Z","timestamp":1666483200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANPCYT","award":["2018-3835, 2019-1442, 2019-1973"],"award-info":[{"award-number":["2018-3835, 2019-1442, 2019-1973"]}]},{"name":"CONICET","award":["0731CO"],"award-info":[{"award-number":["0731CO"]}]},{"name":"UBACYT","award":["2018-0419BA, 2020-0233BA"],"award-info":[{"award-number":["2018-0419BA, 2020-0233BA"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,23]]},"DOI":"10.1145\/3550355.3552462","type":"proceedings-article","created":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T22:44:57Z","timestamp":1666651497000},"page":"289-299","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Predicate abstractions for smart contract validation"],"prefix":"10.1145","author":[{"given":"Javier","family":"Godoy","sequence":"first","affiliation":[{"name":"UBA, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan Pablo","family":"Galeotti","sequence":"additional","affiliation":[{"name":"UBA, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego","family":"Garbervetsky","sequence":"additional","affiliation":[{"name":"UBA, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Uchitel","sequence":"additional","affiliation":[{"name":"UBA, Buenos Aires, Argentina and Imperial College London, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,24]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2016. Analysis of the dao exploit. http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-thedao-exploit\/  2016. Analysis of the dao exploit. http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-thedao-exploit\/"},{"key":"e_1_3_2_1_2_1","unstructured":"2016. The dao smart contract. http:\/\/etherscan.io\/address\/0xbb9bc244d798123fde783fcc1c72d3bb8c189413  2016. The dao smart contract. http:\/\/etherscan.io\/address\/0xbb9bc244d798123fde783fcc1c72d3bb8c189413"},{"key":"e_1_3_2_1_3_1","unstructured":"2017. Azure Blockchain Workbench. https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples  2017. Azure Blockchain Workbench. https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples"},{"issue":"5","key":"e_1_3_2_1_4_1","first-page":"1","article-title":"OMG Unified Modeling Language","volume":"2","year":"2017","unstructured":"2017 . OMG Unified Modeling Language , Version 2 . 5 . 1 . https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF. 2017. OMG Unified Modeling Language, Version 2.5.1. https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF.","journal-title":"Version"},{"key":"e_1_3_2_1_5_1","unstructured":"2018. Smart Contract Best Practices Revisited: Block Number vs. Times-tamp. https:\/\/medium.com\/@phillipgoldberg\/smart-contract-best-practices-revisited-block-number-vs-timestamp-648905104323  2018. Smart Contract Best Practices Revisited: Block Number vs. Times-tamp. https:\/\/medium.com\/@phillipgoldberg\/smart-contract-best-practices-revisited-block-number-vs-timestamp-648905104323"},{"key":"e_1_3_2_1_6_1","unstructured":"2018. Surya's repository. https:\/\/github.com\/ConsenSys\/surya.  2018. Surya's repository. https:\/\/github.com\/ConsenSys\/surya."},{"key":"e_1_3_2_1_7_1","unstructured":"2019. Digital Locker Documentation. https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples\/digital-locker  2019. Digital Locker Documentation. https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples\/digital-locker"},{"key":"e_1_3_2_1_8_1","unstructured":"2020. Azure fixed code. https:\/\/github.com\/blockhousetech\/research\/tree\/master\/Solidifier\/evaluation\/examples\/azure_fixed.  2020. Azure fixed code. https:\/\/github.com\/blockhousetech\/research\/tree\/master\/Solidifier\/evaluation\/examples\/azure_fixed."},{"key":"e_1_3_2_1_9_1","unstructured":"2020. Openzeppelin: Build secure smart contracts in solidity. https:\/\/openzeppelin.com\/contracts\/  2020. Openzeppelin: Build secure smart contracts in solidity. https:\/\/openzeppelin.com\/contracts\/"},{"key":"e_1_3_2_1_10_1","unstructured":"2020. Smart Contract Weakness Classification and Test Cases. https:\/\/swcregistry.io\/  2020. Smart Contract Weakness Classification and Test Cases. https:\/\/swcregistry.io\/"},{"key":"e_1_3_2_1_11_1","unstructured":"2020. Types in Solidity. https:\/\/docs.soliditylang.org\/en\/v0.8.7\/types.html  2020. Types in Solidity. https:\/\/docs.soliditylang.org\/en\/v0.8.7\/types.html"},{"key":"e_1_3_2_1_12_1","unstructured":"2021. Require in Solidity. https:\/\/docs.soliditylang.org\/en\/v0.8.7\/control-structures.html.  2021. Require in Solidity. https:\/\/docs.soliditylang.org\/en\/v0.8.7\/control-structures.html."},{"key":"e_1_3_2_1_13_1","unstructured":"2022. Rust for Near. https:\/\/docs.rs\/near-sdk\/latest\/near_sdk\/macro.require.html.  2022. Rust for Near. https:\/\/docs.rs\/near-sdk\/latest\/near_sdk\/macro.require.html."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2021.3057595"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412841.3442051"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070544"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985846"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.98"},{"key":"e_1_3_2_1_19_1","article-title":"Enabledness-based program abstractions for behavior validation","volume":"22","author":"de Caso G.","year":"2013","unstructured":"G. de Caso , V. Braberman , D. Garbervetsky , and S. Uchitel . 2013 . Enabledness-based program abstractions for behavior validation . ACM Trans. Softw. Eng. Methodol. 22 , 3 (2013). G. de Caso, V. Braberman, D. Garbervetsky, and S. Uchitel. 2013. Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22, 3 (2013).","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2020.2977594"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/EDCC.2018.00036"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/wetseb.2019.00008"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477314.3507309"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070542"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3415153"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3404366"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Alex Groce Josselin Feist Gustavo Grieco and Michael Colburn. 2020. What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?. In Financial Cryptography.  Alex Groce Josselin Feist Gustavo Grieco and Michael Colburn. 2020. What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?. In Financial Cryptography.","DOI":"10.1007\/978-3-030-51280-4_34"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.3390\/su10103652"},{"key":"e_1_3_2_1_34_1","volume-title":"VeriSolid: Correct-by-design smart contracts for Ethereum. arXiv preprint arXiv:1901.01292","author":"Mavridou Anastasia","year":"2019","unstructured":"Anastasia Mavridou , Aron Laszka , Emmanouela Stachtiari , and Abhishek Dubey . 2019. VeriSolid: Correct-by-design smart contracts for Ethereum. arXiv preprint arXiv:1901.01292 ( 2019 ). Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. 2019. VeriSolid: Correct-by-design smart contracts for Ethereum. arXiv preprint arXiv:1901.01292 (2019)."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00133"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_25"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00085"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41600-3_7"},{"key":"e_1_3_2_1_40_1","volume-title":"Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper 151","author":"Gavin Wood","year":"2014","unstructured":"Gavin Wood et al. 2014 . Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper 151 , 2014 (2014), 1--32. Gavin Wood et al. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper 151, 2014 (2014), 1--32."}],"event":{"name":"MODELS '22: ACM\/IEEE 25th International Conference on Model Driven Engineering Languages and Systems","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","Univ. of Montreal University of Montreal","IEEE CS"],"location":"Montreal Quebec Canada","acronym":"MODELS '22"},"container-title":["Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550355.3552462","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3550355.3552462","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:08Z","timestamp":1750183688000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3550355.3552462"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,23]]},"references-count":40,"alternative-id":["10.1145\/3550355.3552462","10.1145\/3550355"],"URL":"https:\/\/doi.org\/10.1145\/3550355.3552462","relation":{},"subject":[],"published":{"date-parts":[[2022,10,23]]},"assertion":[{"value":"2022-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}