{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T14:14:47Z","timestamp":1784556887110,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662588192","type":"print"},{"value":"9783662588208","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-662-58820-8_22","type":"book-chapter","created":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T14:59:45Z","timestamp":1552057185000},"page":"325-338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Proof-Carrying Smart Contracts"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Dickerson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Gazzillo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maurice","family":"Herlihy","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vikram","family":"Saraph","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,2,10]]},"reference":[{"key":"22_CR1","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). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54455-6_8"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11804192_17"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-30569-9_3"},{"key":"22_CR4","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 platform. \nhttp:\/\/why3.lri.fr\/manual.pdf\n\n. Accessed 14 Jan 2018"},{"key":"22_CR5","unstructured":"Daian, P., Breidenbach, L.: Parity proposals\u2019 potential problems. \nhttp:\/\/hackingdistributed.com\/2017\/12\/13\/ether-resurrection\/\n\n. Accessed 14 Jan 2018"},{"key":"22_CR6","unstructured":"DAO: the DAO smart contract. Accessed 8 Feb 2017"},{"key":"22_CR7","unstructured":"Ethereum. \nhttps:\/\/github.com\/ethereum\/\n\n. Accessed 14 Jan 2018"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. In: ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) (2018)","DOI":"10.1145\/3158136"},{"issue":"6","key":"22_CR10","doi-asserted-by":"publisher","first-page":"1049","DOI":"10.1145\/1108970.1108971","volume":"27","author":"M Hicks","year":"2005","unstructured":"Hicks, M., Nettles, S.: Dynamic software updating. ACM Trans. Program. Lang. Syst. 27(6), 1049\u20131096 (2005). \nhttps:\/\/doi.org\/10.1145\/1108970.1108971","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete semantics of the ethereum virtual machine. Technical report (2017)","DOI":"10.1109\/CSF.2018.00022"},{"key":"22_CR12","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"22_CR14","unstructured":"Leroy, X., et al.: The CompCert verified compiler. Documentation and user\u2019s manual, INRIA Paris-Rocquencourt (2012)"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. CCS 2016, pp. 254\u2013269. ACM, New York (2016). \nhttps:\/\/doi.org\/10.1145\/2976749.2978309","DOI":"10.1145\/2976749.2978309"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1997, pp. 106\u2013119. ACM, New York (1997). \nhttps:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"22_CR17","unstructured":"Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. CoRR abs\/1702.05511 (2017). \nhttp:\/\/arxiv.org\/abs\/1702.05511"},{"key":"22_CR18","unstructured":"Sirer, E.G.: Parity\u2019s Wallet Bug is not Alone (2017). \nhttps:\/\/blogs.apache.org\/foundation\/entry\/apache-struts-statement-on-equifax\n\n. Accessed 05 Nov 2017"},{"key":"22_CR19","unstructured":"Various: formal verification for solidity contracts. \nhttps:\/\/forum.ethereum.org\/discussion\/3779\/formal-verification-for-solidity-contracts\n\n. Accessed 14 Jul 2018"},{"key":"22_CR20","unstructured":"Vladimirov, M., Khovratovich, D.: ERC20 API: an attack vector on approve\/transferfrom methods. \nhttps:\/\/docs.google.com\/document\/d\/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM\/edit#heading=h.m9fhqynw2xvt\n\n. Accessed: 14 Jan 2018"},{"key":"22_CR21","unstructured":"The Ethereum Wiki: ERC20 token standard. \nhttps:\/\/theethereum.wiki\/w\/index.php\/ERC20_Token_Standard\n\n. Accessed 14 Jan 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-662-58820-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,5]],"date-time":"2020-11-05T06:11:46Z","timestamp":1604556706000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-58820-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783662588192","9783662588208"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-58820-8_22","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":"10 February 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":"Nieuwpoort","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cura\u00e7ao","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 February 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 March 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fc2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fc18.ifca.ai\/index.html","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":"110","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":"27","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":"2","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":"25% - 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,27","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":"3,27","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)"}}]}}