{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T09:38:20Z","timestamp":1774949900890,"version":"3.50.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031827020","type":"print"},{"value":"9783031827037","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-82703-7_11","type":"book-chapter","created":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T02:17:08Z","timestamp":1737512228000},"page":"231-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Constructing Trustworthy Smart Contracts"],"prefix":"10.1007","author":[{"given":"Devora","family":"Chait-Roth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,1,23]]},"reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In: FM Workshops (1). Lecture Notes in Computer Science, vol. 12232, pp. 368\u2013379. Springer (2019)","DOI":"10.1007\/978-3-030-54994-7_28"},{"key":"11_CR3","unstructured":"Blackshear, S., et al.: Move: a language with programmable resources. https:\/\/developers.diem.com\/papers\/diem-move-a-language-with-programmable-resources\/2019-06-18.pdf"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Br\u00e4m, C., Eilers, M., M\u00fcller, P., Sierra, R., Summers, A.J.: Rich specifications for Ethereum smart contract verification. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201330 (2021)","DOI":"10.1145\/3485523"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Cassez, F., Fuller, J., Quiles, H.M.A.: Deductive verification of smart contracts with dafny. In: FMICS. Lecture Notes in Computer Science, vol. 13487, pp. 50\u201366. Springer (2022)","DOI":"10.1007\/978-3-031-15008-1_5"},{"key":"11_CR6","unstructured":"Hack3d: The web3 security report 2023. At https:\/\/www.certik.com\/resources\/blog\/7BokMhPUgffqEvyvXgHNaq-hack3d-the-web3-security-report-2023"},{"key":"11_CR7","unstructured":"Chait-Roth, D., Namjoshi, K.S.: Constructing trustworthy smart contracts (2024). https:\/\/arxiv.org\/abs\/2411.14563"},{"key":"11_CR8","unstructured":"Crypto investors lost nearly \\$4 billion to hackers in 2022. At https:\/\/www.cnbc.com\/2023\/02\/04\/crypto-investors-lost-nearly-4-billion-dollars-to-hackers-in-2022.html"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Coblenz, M., et al.: Obsidian: typestate and assets for safer blockchain programming. ACM Trans. Program. Lang. Syst. 42(3) (Nov 2020). https:\/\/doi.org\/10.1145\/3417516","DOI":"10.1145\/3417516"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Dill, D., Grieskamp, W., Park, J., Qadeer, S., Xu, M., Zhong, E.: Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. Presented at the (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_10","DOI":"10.1007\/978-3-030-99524-9_10"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: SOLC-verify: a modular verifier for Solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments, Lecture Notes in Computer Science, vol. 12301, pp. 161\u2013179. Springer (2020)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the ethereum virtual machine. In: CSF, pp. 204\u2013217. IEEE Computer Society (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"11_CR13","doi-asserted-by":"publisher","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, pp. 523\u2013540. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: correct-by-design smart contracts for ethereum. In: Goldberg, I., Moore, T. (eds.) FC 2019. LNCS, vol. 11598, pp. 446\u2013465. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016, LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001, LNCS, vol. 2102, pp. 2\u201313. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2","DOI":"10.1007\/3-540-44585-4_2"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001, LNCS, vol. 2245, pp. 292\u2013304. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45294-X_25","DOI":"10.1007\/3-540-45294-X_25"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: VerX: safety verification of smart contracts. In: IEEE Symposium on Security and Privacy (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Hao, K.C.G.: Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3(OOPSLA), 185:1\u2013185:30 (2019)","DOI":"10.1145\/3360611"},{"key":"11_CR21","unstructured":"SMTChecker and Formal Verification for Solidity. At https:\/\/docs.soliditylang.org\/en\/v0.8.23\/smtchecker.html"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: SmartPulse: automated checking of temporal properties in smart contracts. In: IEEE Symposium on Security and Privacy (2021)","DOI":"10.1109\/SP40001.2021.00085"},{"key":"11_CR23","unstructured":"Sun, H., Singh, K., Ramos-D\u00e1vila, J.P., Aldrich, J., DiVincenzo, J.: Gradual verification for smart contracts. In: PriSC (2024). https:\/\/arxiv.org\/pdf\/2311.13351.pdf"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Zhong, J.E., et al.: The move prover. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020, LNCS, vol. 12224, pp. 137\u2013150. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_7","DOI":"10.1007\/978-3-030-53288-8_7"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-82703-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T06:13:56Z","timestamp":1763705636000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-82703-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031827020","9783031827037"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-82703-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denver, CO","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}