{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:54:04Z","timestamp":1764402844323,"version":"3.37.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319898834"},{"type":"electronic","value":"9783319898841"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_26","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T21:02:32Z","timestamp":1523653352000},"page":"739-767","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Quantitative Analysis of Smart Contracts"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Yaron","family":"Velner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-32759-9_1","volume-title":"FM 2012: Formal Methods","author":"M Abadi","year":"2012","unstructured":"Abadi, M.: Software security: a formal perspective. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 1\u20135. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_1"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-44929-9_1","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"M Abadi","year":"2000","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3\u201322. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44929-9_1"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR\u201998 Concurrency Theory","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163\u2013178. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055622"},{"key":"26_CR4","unstructured":"Anonymous Author: King of the ether (2017). www.kingoftheether.com"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Arden, O., Liu, J., Myers, A.C.: Flow-limited authorization. In: CSF, pp. 569\u2013583 (2015)","DOI":"10.1109\/CSF.2015.42"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Arden, O., Myers, A.C.: A calculus for flow-limited authorization. In: CSF (2016)","DOI":"10.1109\/CSF.2016.17"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts. IACR Cryptology ePrint Archive, 1007 (2016)","DOI":"10.1007\/978-3-662-54455-6_8"},{"issue":"1","key":"26_CR8","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s00165-012-0269-9","volume":"26","author":"M Avalle","year":"2014","unstructured":"Avalle, M., Pironti, A., Sisto, R.: Formal verification of security protocol implementations: a survey. Formal Aspects Comput. 26(1), 99\u2013123 (2014)","journal-title":"Formal Aspects Comput."},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: PLAS. ACM (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Chaudhuri, A.: Automated formal analysis of a protocol for secure file sharing on untrusted storage. In: SP, pp. 417\u2013431. IEEE (2008)","DOI":"10.1109\/SP.2008.12"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Bonneau, J., Miller, A., Clark, J., Narayanan, A., Kroll, J.A., Felten, E.W.: Sok: research perspectives and challenges for bitcoin and cryptocurrencies. In: SP, pp. 104\u2013121. IEEE (2015)","DOI":"10.1109\/SP.2015.14"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"1871","key":"26_CR15","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M. Burrows","year":"1989","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. In: Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, pp. 233\u2013271. The Royal Society (1989)","journal-title":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"key":"26_CR16","unstructured":"Buterin, V., et al.: Ethereum white paper (2013)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2011","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243\u2013259. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_20"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Cern\u00fd, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: POPL (2013)","DOI":"10.1145\/2429069.2429085"},{"key":"26_CR19","unstructured":"Chatterjee, K., Goharshady, A.K., Velner, Y.: Quantitative analysis of smart contracts (2018). arXiv preprint: arXiv:1801.03367"},{"key":"26_CR20","unstructured":"Chatterjee, K., Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided planning. In: UAI, pp. 104\u2013111 (2005)"},{"key":"26_CR21","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.ic.2015.03.009","volume":"242","author":"K Chatterjee","year":"2015","unstructured":"Chatterjee, K., Ibsen-Jensen, R.: Qualitative analysis of concurrent mean-payoff games. Inf. Comput. 242, 2\u201324 (2015)","journal-title":"Inf. Comput."},{"key":"26_CR22","unstructured":"Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23\u201335. Institut Mittag-Leffler (1962)"},{"key":"26_CR23","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"26_CR24","unstructured":"CoinMarketCap: Crypto-currency market capitalizations (2017). coinmarketcap.com"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of generalized type unions. In: ACM Conference on Language Design for Reliable Software, vol. 12, pp. 77\u201394. ACM (1977)","DOI":"10.1145\/800022.808314"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269\u2013295. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55844-6_142"},{"key":"26_CR27","unstructured":"Daian, P.: Analysis of the DAO exploit (2016). hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: LICS. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319611"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Delmolino, K., Arnett, M., Kosba, A.E., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab. IACR Cryptology ePrint Archive 2015, 460 (2015)","DOI":"10.1007\/978-3-662-53357-4_6"},{"key":"26_CR30","unstructured":"Ethereum Foundation: Solidity language documentation (2017)"},{"key":"26_CR31","unstructured":"Etherscan: Contract accounts (2017). etherscan.io\/accounts\/c"},{"key":"26_CR32","unstructured":"Etherscan: Token information (2017). etherscan.io\/tokens"},{"key":"26_CR33","unstructured":"ETHNews: Hkg token has a bug and needs to be reissued (2017). ethnews.com\/ethercamps-hkg-token-has-a-bug-and-needs-to-be-reissued"},{"key":"26_CR34","unstructured":"Fuchs, A.P., Chaudhuri, A., Foster, J.S.: Scandroid: automated security certification of android. Technical report (2009)"},{"key":"26_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7"},{"key":"26_CR36","doi-asserted-by":"publisher","first-page":"886","DOI":"10.1007\/3-540-45061-0_69","volume-title":"Automata, Languages and Programming","author":"Thomas A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: ICALP (2003)"},{"key":"26_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-45099-3_12","volume-title":"Static Analysis","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A., Majumdar, R., Mang, F., Raskin, J.-F.: Abstract interpretation of game properties. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 220\u2013239. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-45099-3_12"},{"key":"26_CR38","unstructured":"Jentzsch, C.: Decentralized autonomous organization to automate governance (2016). download.slock.it\/public\/DAO\/WhitePaper.pdf"},{"issue":"4","key":"26_CR39","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"key":"26_CR40","unstructured":"Johnson, N.: A beginner\u2019s guide to buying an ENS domain (2017)"},{"key":"26_CR41","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS, pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"26_CR42","unstructured":"Luu, L., Velner, Y.: Audit report for digix\u2019s smart contract platform (2017)"},{"key":"26_CR43","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)"},{"key":"26_CR44","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"26_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"issue":"1","key":"26_CR46","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"26_CR47","unstructured":"Sapirshtein, A., Sompolinsky, Y., Zohar, A.: Optimal selfish mining strategies in bitcoin (2015). arXiv preprint: arXiv:1507.06183"},{"key":"26_CR48","unstructured":"Simonite, T.: $80 million hack shows the dangers of programmable money, June 2016. www.technologyreview.com"},{"key":"26_CR49","unstructured":"Sompolinsky, Y., Zohar, A.: Bitcoin\u2019s security model revisited. CoRR abs\/1605.09193 (2016)"},{"key":"26_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-662-54970-4_29","volume-title":"Financial Cryptography and Data Security","author":"J Teutsch","year":"2017","unstructured":"Teutsch, J., Jain, S., Saxena, P.: When cryptocurrencies mine their own business? In: Grossklags, J., Preneel, B. (eds.) FC 2016. LNCS, vol. 9603, pp. 499\u2013514. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54970-4_29"},{"key":"26_CR51","unstructured":"Toobin, A.: The DAO, Ethereum\u2019s $150 million blockchain investment fund, has a logic problem (2016). www.inverse.com\/article\/16314-the-dao-ethereum-s-150-million-blockchain"},{"key":"26_CR52","unstructured":"Tran, V., Velner, Y.: Coindash audit report (2017)"},{"key":"26_CR53","unstructured":"Wood, G.: Ethereum yellow paper (2014)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89884-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:33:22Z","timestamp":1571157202000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}