{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T05:17:05Z","timestamp":1781327825106,"version":"3.54.1"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030321000","type":"print"},{"value":"9783030321017","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-32101-7_27","type":"book-chapter","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T11:04:00Z","timestamp":1570791840000},"page":"446-465","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":118,"title":["VeriSolid: Correct-by-Design Smart Contracts for Ethereum"],"prefix":"10.1007","author":[{"given":"Anastasia","family":"Mavridou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aron","family":"Laszka","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emmanouela","family":"Stachtiari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abhishek","family":"Dubey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,9,30]]},"reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-030-01090-4_30","volume-title":"Automated Technology for Verification and Analysis","author":"E Albert","year":"2018","unstructured":"Albert, E., Gordillo, P., Livshits, B., Rubio, A., Sergey, I.: EthIR: a framework for high-level analysis of Ethereum bytecode. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 513\u2013520. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_30"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","volume-title":"Principles of Security and Trust","author":"N Atzei","year":"2017","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58387-6_29","volume-title":"Financial Cryptography and Data Security","author":"N Atzei","year":"2018","unstructured":"Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of Bitcoin transactions. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_29"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1007\/978-3-319-70278-0_31","volume-title":"Financial Cryptography and Data Security","author":"M Bartoletti","year":"2017","unstructured":"Bartoletti, M., Pompianu, L.: An empirical analysis of smart contracts: platforms, applications, and design patterns. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 494\u2013509. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_31"},{"issue":"3","key":"27_CR5","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Short paper: formal verification of smart contracts. In: Proceedings of the 11th ACM Workshop on Programming Languages and Analysis for Security (PLAS), in Conjunction with ACM CCS 2016, pp. 91\u201396, October 2016","DOI":"10.1145\/2993600.2993611"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-319-24953-7_25","volume-title":"Automated Technology for Verification and Analysis","author":"S Bliudze","year":"2015","unstructured":"Bliudze, S., et al.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326\u2013343. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_25"},{"key":"27_CR8","unstructured":"Brent, L., et al.: Vandal: a scalable security analysis framework for smart contracts. arXiv preprint arXiv:1809.03981 (2018)"},{"key":"27_CR9","doi-asserted-by":"publisher","first-page":"2292","DOI":"10.1109\/ACCESS.2016.2566339","volume":"4","author":"K Christidis","year":"2016","unstructured":"Christidis, K., Devetsikiotis, M.: Blockchains and smart contracts for the Internet of Things. IEEE Access 4, 2292\u20132303 (2016)","journal-title":"IEEE Access"},{"key":"27_CR10","unstructured":"Clack, C.D., Bakshi, V.A., Braine, L.: Smart contract templates: foundations, design landscape and research directions. arXiv preprint arXiv:1608.00771 (2016)"},{"issue":"5","key":"27_CR11","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-03427-6_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"C Colombo","year":"2018","unstructured":"Colombo, C., Ellul, J., Pace, G.J.: Contracts over smart contracts: recovering from violations dynamically. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 300\u2013315. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_23"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Ellul, J., Pace, G.: Runtime verification of Ethereum smart contracts. In: Workshop on Blockchain Dependability (WBD), in Conjunction with 14th European Dependable Computing Conference (EDCC) (2018)","DOI":"10.1109\/EDCC.2018.00036"},{"key":"27_CR14","unstructured":"Finley, K.: A \\$50 million hack just showed that the DAO was all too human. Wired. https:\/\/www.wired.com\/2016\/06\/50-million-hack-just-showed-dao-human\/ (2016)"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Frantz, C.K., Nowostawski, M.: From institutions to code: towards automated generation of smart contracts. In: 1st IEEE International Workshops on Foundations and Applications of Self* Systems (FAS*W), pp. 210\u2013215. IEEE (2016)","DOI":"10.1109\/FAS-W.2016.53"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-67816-0_20","volume-title":"Data Privacy Management, Cryptocurrencies and Blockchain Technology","author":"M Fr\u00f6wis","year":"2017","unstructured":"Fr\u00f6wis, M., B\u00f6hme, R.: In code we trust? In: Garcia-Alfaro, J., Navarro-Arribas, G., Hartenstein, H., Herrera-Joancomart\u00ed, J. (eds.) ESORICS\/DPM\/CBT -2017. LNCS, vol. 10436, pp. 357\u2013372. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-67816-0_20"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"27_CR18","first-page":"243","volume-title":"Lecture Notes in Computer Science","author":"Ilya Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. Technical report, TU Wien (2018)"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete semantics of the Ethereum virtual machine. Technical report, UIUC (2017)","DOI":"10.1109\/CSF.2018.00022"},{"key":"27_CR20","unstructured":"Hirai, Y.: Formal verification of deed contract in Ethereum name service, November 2016. https:\/\/yoichihirai.com\/deed.pdf"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Hu, J., Zhong, Y.: A method of logic-based smart contracts for blockchain system. In: Proceedings of the 4th International Conference on Data Processing and Applications (ICPDA), pp. 58\u201361. ACM (2018)","DOI":"10.1145\/3224207.3224218"},{"key":"27_CR23","volume-title":"Principles of Database and Knowledge-base Systems","author":"DU Jeffrey","year":"1989","unstructured":"Jeffrey, D.U.: Principles of Database and Knowledge-base Systems. Computer Science Press, New york (1989)"},{"key":"27_CR24","unstructured":"Jiao, J., Kan, S., Lin, S.W., Sanan, D., Liu, Y., Sun, J.: Executable operational semantics of Solidity. arXiv preprint arXiv:1804.01295 (2018)"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 254\u2013269. ACM, October 2016","DOI":"10.1145\/2976749.2978309"},{"key":"27_CR26","unstructured":"Mar\u00f3ti, M., et al.: Next generation (meta) modeling: web-and cloud-based collaborative tool infrastructure. In: Proceedings of the MPM@ MoDELS, pp. 41\u201360 (2014)"},{"key":"27_CR27","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58387-6_28","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2018","unstructured":"Mavridou, A., Laszka, A.: Designing secure Ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28"},{"key":"27_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-89722-6_11","volume-title":"Principles of Security and Trust","author":"A Mavridou","year":"2018","unstructured":"Mavridou, A., Laszka, A.: Tool demonstration: FSolidM for designing secure ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 270\u2013277. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_11"},{"key":"27_CR29","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: Verisolid: correct-by-design smart contracts for Ethereum. arXiv preprint arXiv:1901.01292 (2019). https:\/\/arxiv.org\/pdf\/1901.01292.pdf"},{"key":"27_CR30","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency, vol. 84. Prentice Hall, New York (1989)"},{"key":"27_CR31","unstructured":"Mueller, B.: Smashing Ethereum smart contracts for fun and real profit. In: 9th Annual HITB Security Conference (HITBSecConf) (2018)"},{"key":"27_CR32","unstructured":"Newman, L.H.: Security news this week: \\$280m worth of Ethereum is trapped thanks to a dumb bug. Wired, November 2017. https:\/\/www.wired.com\/story\/280m-worth-of-ethereum-is-trapped-for-a-pretty-dumb-reason\/"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: 34th Annual Computer Security Applications Conference (ACSAC) (2018)","DOI":"10.1145\/3274694.3274743"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-15317-9_18","volume-title":"Formal Aspects of Component Software","author":"M Noureddine","year":"2015","unstructured":"Noureddine, M., Jaber, M., Bliudze, S., Zaraket, F.A.: Reduction and abstraction techniques for BIP. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 288\u2013305. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15317-9_18"},{"key":"27_CR35","doi-asserted-by":"publisher","unstructured":"O\u2019Connor, R.: Simplicity: a new language for blockchains. In: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS 2017, pp. 107\u2013120. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3139337.3139340","DOI":"10.1145\/3139337.3139340"},{"key":"27_CR36","unstructured":"Parizi, R.M., Dehghantanha, A., Choo, K.K.R., Singh, A.: Empirical vulnerability analysis of automated smart contracts security testing on blockchains. In: 28th Annual International Conference on Computer Science and Software Engineering (CASCON) (2018)"},{"key":"27_CR37","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Computer Science Department, Aarhus University, Denmark (1981)"},{"key":"27_CR38","unstructured":"Solidity by example: blind auction (2018). https:\/\/solidity.readthedocs.io\/en\/develop\/solidity-by-example.html#blind-auction . Accessed 25 Sept 2018"},{"key":"27_CR39","unstructured":"Solidity documentation: common patterns (2018). http:\/\/solidity.readthedocs.io\/en\/develop\/common-patterns.html#state-machine . Accessed 25 Sept 2018"},{"key":"27_CR40","unstructured":"Solidity documentation: security considerations - use the checks-effects-interactions pattern (2018). http:\/\/solidity.readthedocs.io\/en\/develop\/security-considerations.html#use-the-checks-effects-interactions-pattern . Accessed 25 Sept 2018"},{"key":"27_CR41","unstructured":"Stortz, R.: Rattle - an Ethereum EVM binary analysis framework. In: REcon, Montreal (2018)"},{"key":"27_CR42","doi-asserted-by":"crossref","unstructured":"Tsankov, P., Dan, A., Cohen, D.D., Gervais, A., Buenzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: 25th ACM Conference on Computer and Communications Security (CCS) (2018)","DOI":"10.1145\/3243734.3243780"},{"issue":"11","key":"27_CR43","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2994581","volume":"59","author":"S Underwood","year":"2016","unstructured":"Underwood, S.: Blockchain beyond Bitcoin. Commun. ACM 59(11), 15\u201317 (2016)","journal-title":"Commun. ACM"},{"key":"27_CR44","doi-asserted-by":"crossref","unstructured":"W\u00f6hrer, M., Zdun, U.: Design patterns for smart contracts in the Ethereum ecosystem. In: Proceedings of the 2018 IEEE Conference on Blockchain, pp. 1513\u20131520 (2018)","DOI":"10.1109\/Cybermatics_2018.2018.00255"},{"key":"27_CR45","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Technical report, EIP-150, Ethereum Project - Yellow Paper, April 2014"},{"key":"27_CR46","unstructured":"Yang, Z., Lei, H.: Lolisa: formal syntax and semantics for a subset of the solidity programming language. arXiv preprint arXiv:1803.09885 (2018)"}],"container-title":["Lecture Notes in Computer Science","Financial Cryptography and Data Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32101-7_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,24]],"date-time":"2021-01-24T15:03:42Z","timestamp":1611500622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-32101-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030321000","9783030321017"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27","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":"30 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Financial Cryptography and Data Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"St. Kitts","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Saint Kitts and Nevis","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":"18 February 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 February 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fc19.ifca.ai\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"178","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":"32","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":"18% - 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,08","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":"7,6","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)"}}]}}