{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:56Z","timestamp":1762459676113},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319980461"},{"type":"electronic","value":"9783319980478"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_1","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"1-18","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Smart Contracts: A Killer Application for Deductive Source Code Verification"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Ahrendt","sequence":"first","affiliation":[]},{"given":"Gordon J.","family":"Pace","sequence":"additional","affiliation":[]},{"given":"Gerardo","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"1_CR1","unstructured":"A. Hern. $300m in cryptocurrency accidentally lost forever due to bug. Appeared at The Guardian https:\/\/www.theguardian.com\/technology\/2017\/nov\/08\/cryptocurrency-300m-dollars-stolen-bug-ether . Nov. 2017."},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"T. Abdellatif and K. L. Brousmiche. \u201cFormal Verification of Smart Contracts Based on Users and Blockchain Behaviors Models. In 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS). Feb. 2018, pp. 1\u20135. https:\/\/doi.org\/10.1109\/NTMS.2018.8328737 .","DOI":"10.1109\/NTMS.2018.8328737"},{"key":"1_CR3","unstructured":"Wolfgang Ahrendt et al., eds. Deductive Software Verification\u2014The KeY Book. Vol. 10001. LNCS. Springer, 2016."},{"key":"1_CR4","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"Wolfgang Ahrendt","year":"2014","unstructured":"Wolfgang Ahrendt et al. \u201cThe KeY Platform for Verification and Analysis of Java Programs\u201d. In: STTE\u201914. Vol. 8471. LNCS. Springer, 2014, pp. 55\u201371. https:\/\/doi.org\/10.1007\/978-3-319-12154-3_4 ."},{"key":"1_CR5","first-page":"164","volume-title":"Lecture Notes in Computer Science","author":"Nicola Atzei","year":"2017","unstructured":"Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. \u201cA Survey of Attacks on Ethereum Smart Contracts (SoK)\u201d. In: Proceedings of the 6th International Conference on Principles of Security and Trust. Vol. 10204. LNCS. Springer, 2017. ISBN: 978-3-662-54454-9. URL: https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8 ."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Xiaomin Bai et al. \u201cFormal Modeling and Verification of Smart Contracts\u201d. In: Proceedings of the 2018 7th International Conference on Software and Computer Applications. ICSCA 2018. Kuantan, Malaysia: ACM, 2018, pp. 322\u2013326. ISBN: 978-1-4503-5414-1. https:\/\/doi.org\/10.1145\/3185089.3185138 . URL: http:\/\/doi.acm.org\/10.1145\/3185089.3185138 .","DOI":"10.1145\/3185089.3185138"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Michael Barnett et al. \u201cBoogie: A Modular Reusable Verifier for Object-Oriented Programs\u201d. In: Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, 2005, Revised Lectures. Ed. by Frank S. de Boer et al. Vol. 4111. LNCS. Springer, 2006.","DOI":"10.1007\/11804192_17"},{"key":"1_CR8","unstructured":"Bernhard Beckert, Vladimir Klebanov, and Benjamin Wei\u00df. \u201cDynamic Logic for Java\u201d. In: Deductive Software Verification\u2014The KeY Book. Vol. 10001. LNCS. Springer, 2016."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan et al. \u201cFormal Verification of Smart Contracts: Short Paper\u201d. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. PLAS \u201916. Vienna, Austria: ACM, 2016. ISBN: 978-1-4503-4574-3. https:\/\/doi.org\/10.1145\/2993600.2993611 . URL: http:\/\/doi.acm.org\/10.1145\/2993600.2993611 .","DOI":"10.1145\/2993600.2993611"},{"key":"1_CR10","unstructured":"Lorenz Breidenbach et al. An in-depth look at the parity multisig bug. Appeared at \u201cHacking, Distributed\u201d http:\/\/hackingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug . June 2016."},{"key":"1_CR11","unstructured":"Crystal Chang Din, Richard Bubel, and Reiner H\u00e4hnle. \u201cKeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS\u201d. In: Automated Deduction - CADE-25. Springer, 2015."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Joshua Ellul and Gordon J. Pace. \u201cCONTRACTLARVA: Runtime Verification of Ethereum Smart Contracts\u201d. In: submitted for review. 2018.","DOI":"10.1109\/EDCC.2018.00036"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Michael Fr\u00f6wis and Rainer B\u00f6hme. \u201cIn Code We Trust?\u201d In: Data Privacy Management, Cryptocurrencies and Blockchain Technology. Ed. by Joaquin Garcia-Alfaro et al. Vol. 10436. LNCS. 2017.","DOI":"10.1007\/978-3-319-67816-0"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Luciano Garc\u00eda-Ba\u00f1uelos et al. \u201cOptimized Execution of Business Processes on Blockchain\u201d. In: Business Process Management. Ed. by Josep Carmona, Gregor Engels, and Akhil Kumar. Vol. 10445. LNCS. 2017.","DOI":"10.1007\/978-3-319-65000-5"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Stijn de Gouw et al. \u201cOpenJDK\u2019s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case\u201d. In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, USA, July 2015. 2015.","DOI":"10.1007\/978-3-319-21690-4_16"},{"key":"1_CR16","unstructured":"Guido Governatori et al. \u201cOn legal contracts, imperative and declarative smart contracts, and blockchain systems\u201d. In: Artificial Intelligence and Law (Mar. 2018), pp. 1\u201333."},{"key":"1_CR17","unstructured":"Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. \u201cA Semantic Framework for the Security Analysis of Ethereum Smart Contracts\u201d. In: POST. Vol. 10804. Lecture Notes in Computer Science. Springer, 2018, pp. 243\u2013269."},{"key":"1_CR18","unstructured":"Everett Hildenbrandt et al. KEVM: A Complete Semantics of the Ethereum Virtual Machine. White paper. 2017. URL: http:\/\/hdl.handle.net\/2142\/97207 ."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Yoichi Hirai. \u201cDefining the Ethereum Virtual Machine for Interactive Theorem Provers\u201d. In: Financial Cryptography Workshops. Vol. 10323. Lecture Notes in Computer Science. Springer, 2017, pp. 520\u2013535.","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Marieke Huisman et al. \u201cFormal Specification with the Java Modeling Language\u201d. In: Deductive Software Verification\u2014The KeY Book. Vol. 10001. LNCS. Springer, 2016.","DOI":"10.1007\/978-3-319-49812-6_7"},{"key":"1_CR21","unstructured":"Florian Idelberger et al. \u201cEvaluation of Logic-Based Smart Contracts for Blockchain Systems\u201d. In: Rule Technologies. Research, Tools, and Applications. Ed. by Jose Julio Alferes et al. Vol. 9718. LNCS. Springer, 2016. ISBN: 978-3-319-42019-6."},{"key":"1_CR22","unstructured":"Nikolai Kosmatov, Virgile Prevosto, and Julien Signoles. \u201cA Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper\u201d. In: Tests and Proofs. Ed. by Margus Veanes and Luca Vigan\u00f2. Springer, 2013. ISBN: 978-3-642-38916-0."},{"key":"1_CR23","unstructured":"Martin Leucker and Christian Schallhart. \u201cA brief account of runtime verification\u201d. In: The Jour. of Logic and Algebraic Progr. 78.5 (2009). The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS\u201907), pp. 293\u2013303. ISSN: 1567-8326."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Loi Luu et al. \u201cMaking Smart Contracts Smarter\u201d. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. CCS \u201916. Vienna, Austria: ACM, 2016, pp. 254\u2013269. ISBN: 978-1-4503-4139-4. https:\/\/doi.org\/10.1145\/2976749.2978309 . URL: http:\/\/doi.acm.org\/10.1145\/2976749.2978309 .","DOI":"10.1145\/2976749.2978309"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Andrew Miller, Zhicheng Cai, and Somesh Jha. \u201cSmart Contracts and Opportunities for Formal Methods\u201d. In: ISoLA\u201918. LNCS. To appear. Springer, 2018.","DOI":"10.1007\/978-3-030-03427-6_22"},{"key":"1_CR26","unstructured":"Mix. Ethereum bug causes integer overflow in numerous ERC20 smart contracts (Update). Appeared at HardFork https:\/\/thenextweb.com\/hardfork\/2018\/04\/25\/ethereum-smart-contract-integer-overflow\/ . Apr. 2018."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Wojciech Mostowski. \u201cVerifying Java Card Programs\u201d. In: Deductive Software Verification\u2014 The KeY Book. Vol. 10001. LNCS. Springer, 2016.","DOI":"10.1007\/978-3-319-49812-6_10"},{"key":"1_CR28","unstructured":"Bernhard Mueller. \u201cSmashing Ethereum Smart Contracts for Fun and Real Profit\u201d. In: HITB SECCONF Amsterdam. 2018."},{"key":"1_CR29","unstructured":"Satoshi Nakamoto. \u201cBitcoin: A peer-to-peer electronic cash system\u201d. 2009. URL: http:\/\/bitcoin.org\/bitcoin.pdf ."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Ivica Nikoli\u0107 et al. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. Unpublished, submitted, available at arXiv:1802.06038. 2018.","DOI":"10.1145\/3274694.3274743"},{"key":"1_CR31","unstructured":"Christoph Prybila et al. \u201cRuntime Verification for Business Processes Utilizing the Bitcoin Blockchain\u201d. In: CoRR abs\/1706.04404 (2017). arXiv: 1706.04404. URL: http:\/\/arxiv.org\/abs\/1706.04404 ."},{"key":"1_CR32","unstructured":"Haseeb Qureshi. A hacker stole $31M of Ether - how it happened, and what it means for Ethereum. Appeared at FreeCodeCamp https:\/\/medium.freecodecamp.org\/a-hacker-stole-31m-of-ether-how-it-happened-and-what-it-means-for-ethereum-9e5dc29e33ce . July 2017."},{"key":"1_CR33","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"Willem-Paul Roever de","year":"2001","unstructured":"Willem-Paul de Roever et al. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, 2001."},{"key":"1_CR34","unstructured":"Philipp R\u00fcmmer and Mattias Ulbrich. \u201cProof Search with Taclets\u201d. In: Deductive Software Verification\u2014The KeY Book. Vol. 10001. LNCS. Springer, 2016."},{"key":"1_CR35","unstructured":"Ilya Sergey and Aquinas Hobor. \u201cA Concurrent Perspective on Smart Contracts\u201d. In: Financial Cryptography and Data Security. Ed. by Michael Brenner et al. Vol. 10395. LNCS. Springer, 2017."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Ingo Weber et al. \u201cUntrusted Business Process Monitoring and Execution Using Blockchain\u201d. In: Formal Techniques for Distributed Systems. Vol. 9850. LNCS. Springer, 2016.","DOI":"10.1007\/978-3-319-45348-4_19"},{"key":"1_CR37","unstructured":"David Z. Morris. Blockchain-based venture capital fund hacked for $60 million. Appeared at Fortune.com http:\/\/fortune.com\/2016\/06\/18\/blockchain-vc-fund-hacked . June 2016."}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,6]],"date-time":"2023-09-06T05:04:18Z","timestamp":1693976658000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_1","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}