{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T12:23:05Z","timestamp":1763727785403,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030549930"},{"type":"electronic","value":"9783030549947"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-54994-7_28","type":"book-chapter","created":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T20:03:45Z","timestamp":1597262625000},"page":"368-379","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Bernardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rapha\u00ebl","family":"Cauderlier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenlei","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Basile","family":"Pesin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Tesson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,8,13]]},"reference":[{"key":"28_CR1","unstructured":"Michelson: the language of Smart Contracts in Tezos. \nhttps:\/\/tezos.gitlab.io\/whitedoc\/michelson.html"},{"key":"28_CR2","unstructured":"Proof-of-stake in Tezos. \nhttps:\/\/tezos.gitlab.io\/whitedoc\/proof_of_stake.html"},{"key":"28_CR3","unstructured":"Tezos code repository. \nhttps:\/\/gitlab.com\/tezos\/tezos"},{"key":"28_CR4","unstructured":"An introduction to the zen protocol. \nhttps:\/\/www.zenprotocol.com\/files\/zen_protocol_white_paper.pdf\n\n (2017)"},{"key":"28_CR5","unstructured":"Ahman, D., et al.: Dijkstra monads for free. CoRR abs\/1608.06499 (2016). \nhttp:\/\/arxiv.org\/abs\/1608.06499"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"28_CR7","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper, pp. 91\u201396. PLAS 2016. ACM, New York (2016). \nhttps:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"issue":"1\u20132","key":"28_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/3300000004","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1(1\u20132), 1\u2013135 (2016). \nhttps:\/\/doi.org\/10.1561\/3300000004","journal-title":"Found. Trends Priv. Secur."},{"key":"28_CR9","unstructured":"Breitman, A.: Multisig contract in Michelson. \nhttps:\/\/github.com\/murbard\/smart-contracts\/blob\/master\/multisig\/michelson\/generic_multisig.tz"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: ICFP 2011, pp. 418\u2013430. ACM, New York (2011)","DOI":"10.1145\/2034574.2034828"},{"key":"28_CR11","unstructured":"Claret, G.: Program in Coq. Theses, Universit\u00e9 Paris Diderot - Paris 7, September 2018. \nhttps:\/\/hal.inria.fr\/tel-01890983"},{"issue":"8","key":"28_CR12","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). \nhttps:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"28_CR13","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, Jean-Christophe, Paskevich, Andrei: Why3\u2014where programs meet provers. In: Felleisen, Matthias, Gardner, Philippa (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_8\n\n. \nhttps:\/\/hal.inria.fr\/hal-00789533","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"28_CR14","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":"Ilya Grishchenko","year":"2018","unstructured":"Grishchenko, Ilya, Maffei, Matteo, Schneidewind, Clara: A semantic framework for the security analysis of ethereum smart contracts. In: Bauer, Lujo, K\u00fcsters, Ralf (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete semantics of the ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium, pp. 204\u2013217. IEEE (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"28_CR16","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The OCaml system release 4.08: documentation and user\u2019s manual. User manual, Inria, June 2019. \nhttp:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant forHigher-Order Logic","year":"2002","unstructured":"Nipkow, Tobias, Wenzel, Markus, Paulson, Lawrence C. (eds.): Isabelle\/HOL: A Proof Assistant forHigher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"28_CR18","doi-asserted-by":"publisher","unstructured":"Pessaux, F.: FoCaLiZe: inside an F-IDE. In: Workshop F-IDE 2014. Proceedings F-IDE 2014, Grenoble, France, May 2014. \nhttps:\/\/doi.org\/10.4204\/EPTCS.149.7","DOI":"10.4204\/EPTCS.149.7"},{"key":"28_CR19","unstructured":"Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contract intermediate-level language. CoRR abs\/1801.00687 (2018). \nhttp:\/\/arxiv.org\/abs\/1801.00687"},{"issue":"OOPSLA","key":"28_CR20","doi-asserted-by":"publisher","first-page":"185:1","DOI":"10.1145\/3360611","volume":"3","author":"I Sergey","year":"2019","unstructured":"Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Hao, K.C.G.: Safer smart contract programming with scilla. PACMPL 3(OOPSLA), 185:1\u2013185:30 (2019). \nhttps:\/\/doi.org\/10.1145\/3360611","journal-title":"PACMPL"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: POPL, pp. 256\u2013270. ACM, January 2016. \nhttps:\/\/www.fstar-lang.org\/papers\/mumon\/","DOI":"10.1145\/2914770.2837655"},{"key":"28_CR22","unstructured":"The Coq development team: The Coq Reference Manual, version 8.9, November 2018. \nhttp:\/\/coq.inria.fr\/doc"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. Cryptology ePrint Archive, Report 2017\/536","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Formal Methods. FM 2019 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-54994-7_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T20:09:51Z","timestamp":1597262991000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-54994-7_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030549930","9783030549947"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54994-7_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/?page_id=84","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","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":"44","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":"34% - 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":"4","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":"5,5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}