{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:01Z","timestamp":1776316861712,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309411","type":"print"},{"value":"9783030309428","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_35","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"593-610","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain"],"prefix":"10.1007","author":[{"given":"Theodoros","family":"Kasampalis","sequence":"first","affiliation":[]},{"given":"Dwight","family":"Guth","sequence":"additional","affiliation":[]},{"given":"Brandon","family":"Moore","sequence":"additional","affiliation":[]},{"given":"Traian Florin","family":"\u0218erb\u0103nu\u021b\u0103","sequence":"additional","affiliation":[]},{"given":"Yi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Daniele","family":"Filaretti","sequence":"additional","affiliation":[]},{"given":"Virgil","family":"\u0218erb\u0103nu\u021b\u0103","sequence":"additional","affiliation":[]},{"given":"Ralph","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"35_CR1","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts. IACR Cryptology ePrint Archive 2016, 1007 (2016). \nhttps:\/\/eprint.iacr.org\/2016\/1007.pdf"},{"key":"35_CR2","unstructured":"Blockstream: Simplicity blog post and resources (2019). \nhttps:\/\/blockstream.com\/2018\/11\/28\/en-simplicity-github\/"},{"key":"35_CR3","doi-asserted-by":"publisher","unstructured":"Bogdanas, D., Rosu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL2015), pp. 445\u2013456. ACM, January 2015. \nhttps:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"35_CR4","unstructured":"Breidenbach, L., Daian, P., Juels, A., Sirer, E.G.: An in-depth look at the parity multisig bug (2017). \nhttp:\/\/hackingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug\/"},{"key":"35_CR5","unstructured":"Buterin, V., Ethereum Foundation: Ethereum White Paper (2013). \nhttps:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper"},{"key":"35_CR6","doi-asserted-by":"publisher","unstructured":"\u015etef\u0103nescu, A., Park, D., Yuwen, S., Li, Y., Ro\u015fu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), pp. 74\u201391. ACM, November 2016. \nhttps:\/\/doi.org\/10.1145\/2983990.2984027","DOI":"10.1145\/2983990.2984027"},{"key":"35_CR7","unstructured":"Daian, P.: DAO attack (2016). \nhttp:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"35_CR9","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 533\u2013544. ACM, January 2012. \nhttps:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"35_CR10","unstructured":"Ethereum: Ethereum C++ Client (2019). \nhttps:\/\/github.com\/ethereum\/cpp-ethereum"},{"key":"35_CR11","unstructured":"Ethereum: Solidity documentation (2019). \nhttp:\/\/solidity.readthedocs.io"},{"key":"35_CR12","unstructured":"Ethereum: Vyper documentation (2019). \nhttps:\/\/vyper.readthedocs.io"},{"key":"35_CR13","unstructured":"Etherscan: Ethereum Transaction Growth (2019). \nhttps:\/\/etherscan.io\/chart\/tx"},{"key":"35_CR14","doi-asserted-by":"publisher","unstructured":"Hathhorn, C., Ellison, C., Rosu, G.: Defining the undefinedness of C. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 336\u2013345. ACM, June 2015. \nhttps:\/\/doi.org\/10.1145\/2813885.2737979","DOI":"10.1145\/2813885.2737979"},{"key":"35_CR15","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete semantics of the Ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium, pp. 204\u2013217. IEEE (2018). \nhttps:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"35_CR16","unstructured":"IOHK: IELE Testnet (2019). \nhttps:\/\/testnet.iohkdev.io\/iele\/"},{"key":"35_CR17","unstructured":"IOHK: KEVM Testnet (2019). \nhttps:\/\/testnet.iohkdev.io\/kevm\/"},{"key":"35_CR18","unstructured":"IOHK: Mantis Ethereum Classic Client (2019). \nhttps:\/\/iohk.io\/blog\/mantis-ethereum-classic-beta-release"},{"key":"35_CR19","unstructured":"IOHK: Plutus testnet (2019). \nhttps:\/\/testnet.iohkdev.io\/plutus\/"},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"Kasampalis, T., et al.: IELE: a rigorously designed language and tool ecosystem for the blockchain. Technical report, University of Illinois, July 2019. \nhttp:\/\/hdl.handle.net\/2142\/104601","DOI":"10.1007\/978-3-030-30942-8_35"},{"key":"35_CR21","unstructured":"KEVM: Jello paper (2019). \nhttps:\/\/jellopaper.org\/"},{"key":"35_CR22","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization, CGO 2004, p. 75. IEEE Computer Society, Washington, DC, USA (2004). \nhttp:\/\/llvm.org"},{"key":"35_CR23","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML: Revised","author":"R Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML: Revised. MIT Press, Cambridge (1997)"},{"key":"35_CR24","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). \nhttps:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"35_CR25","doi-asserted-by":"publisher","unstructured":"Park, D., Stefanescu, A., Rosu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 346\u2013356. ACM, June 2015. \nhttps:\/\/doi.org\/10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"key":"35_CR26","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 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE 2018). ACM, November 2018. \nhttps:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"35_CR27","unstructured":"PeckShield: New batchOverflow Bug in Multiple ERC20 Smart Contracts (CVE-2018-10299) (2018). \nhttps:\/\/medium.com\/coinmonks\/alert-new-batchoverflow-bug-in-multiple-erc20-smart-contracts-cve-2018-10299-511067db6536"},{"key":"35_CR28","unstructured":"RChain Cooperative: Rchain and rholang documentation (2019). \nhttps:\/\/architecture-docs.readthedocs.io\/"},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010). \nhttp:\/\/kframework.org","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"35_CR30","unstructured":"RuntimeVerification: ERC20-K: Formal Executable Specification of ERC20 (2017). \nhttps:\/\/github.com\/runtimeverification\/erc20-semantics"},{"key":"35_CR31","unstructured":"RuntimeVerification: ERC20 Token in IELE (2019). \nhttps:\/\/github.com\/runtimeverification\/iele-semantics\/blob\/master\/iele-examples\/erc20.iele"},{"key":"35_CR32","unstructured":"RuntimeVerification: Formal Smart Contract Verification (2019). \nhttps:\/\/runtimeverification.com\/smartcontract\/"},{"key":"35_CR33","unstructured":"RuntimeVerification: The formal semantics for IELE \u2013 source code (2019). \nhttps:\/\/github.com\/runtimeverification\/iele-semantics"},{"key":"35_CR34","unstructured":"Solana, J.: \\$500K hack challenge backfires on blockchain lottery SmartBillions (2017). \nhttps:\/\/calvinayre.com\/2017\/10\/13\/bitcoin\/500k-hack-challenge-backfires-blockchain-lottery-smartbillions\/"},{"key":"35_CR35","unstructured":"Steiner, J.: Security is a process: a postmortem on the parity multi-sig library self-destruct (2017). \nhttp:\/\/goo.gl\/LBh1vR"},{"key":"35_CR36","unstructured":"Tezos: Michelson documentation (2019). \nhttps:\/\/tezos.gitlab.io\/master\/index.html"},{"key":"35_CR37","unstructured":"The Ethereum Foundation: ERC20 token standard (2019). \nhttps:\/\/github.com\/ethereum\/EIPs\/blob\/master\/EIPS\/eip-20-token-standard.md"},{"key":"35_CR38","first-page":"1","volume":"151","author":"G Wood","year":"2014","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1\u201332 (2014)","journal-title":"Ethereum Proj. Yellow Pap."},{"key":"35_CR39","unstructured":"Zilliqa: Scilla language webpage (2019). \nhttps:\/\/scilla-lang.org\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:11:52Z","timestamp":1588659112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","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":"129","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":"44","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":"7","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":"34% - 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":"4","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":"5,5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}