{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T06:58:56Z","timestamp":1781333936956,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":9,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,10,24]],"date-time":"2016-10-24T00:00:00Z","timestamp":1477267200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,10,24]]},"DOI":"10.1145\/2993600.2993611","type":"proceedings-article","created":{"date-parts":[[2016,10,25]],"date-time":"2016-10-25T12:46:35Z","timestamp":1477399595000},"page":"91-96","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":510,"title":["Formal Verification of Smart Contracts"],"prefix":"10.1145","author":[{"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Delignat-Lavaud","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anitha","family":"Gollamudi","sequence":"additional","affiliation":[{"name":"Harvard University, Cambridge, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georges","family":"Gonthier","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nadim","family":"Kobeissi","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natalia","family":"Kulatova","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bangalore, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Sibut-Pinote","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,10,24]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_1_2_1","volume-title":"Critical update re: Dao vulnerability. https:\/\/blog.ethereum.org\/2016\/06\/17\/critical-update-re-dao-vulnerability","author":"Buterin V.","year":"2016","unstructured":"V. Buterin . Critical update re: Dao vulnerability. https:\/\/blog.ethereum.org\/2016\/06\/17\/critical-update-re-dao-vulnerability , 2016 . V. Buterin. Critical update re: Dao vulnerability. https:\/\/blog.ethereum.org\/2016\/06\/17\/critical-update-re-dao-vulnerability, 2016."},{"key":"e_1_3_2_1_3_1","unstructured":"Ethereum. Solidity documentation -- Release 0.2.0. http:\/\/solidity.readthedocs.io\/ 2016.  Ethereum. Solidity documentation -- Release 0.2.0. http:\/\/solidity.readthedocs.io\/ 2016."},{"key":"e_1_3_2_1_4_1","volume-title":"https:\/\/ethereum.github.io\/browser-solidity","year":"2016","unstructured":"Ethereum. Solidity-browser. https:\/\/ethereum.github.io\/browser-solidity , 2016 . Ethereum. Solidity-browser. https:\/\/ethereum.github.io\/browser-solidity, 2016."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_7_1","unstructured":"S. Nakamoto. Bitcoin: A peer-to-peer electronic cash system. http:\/\/bitcoin.org\/bitcoin.pdf.  S. Nakamoto. Bitcoin: A peer-to-peer electronic cash system. http:\/\/bitcoin.org\/bitcoin.pdf."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535889"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_10_1","unstructured":"G. Wood. Ethereum: A secure decentralised generalised transaction ledger. http:\/\/gavwood.com\/paper.pdf.  G. Wood. Ethereum: A secure decentralised generalised transaction ledger. http:\/\/gavwood.com\/paper.pdf."}],"event":{"name":"CCS'16: 2016 ACM SIGSAC Conference on Computer and Communications Security","location":"Vienna Austria","acronym":"CCS'16","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2993600.2993611","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2993600.2993611","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:23Z","timestamp":1750218623000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2993600.2993611"}},"subtitle":["Short Paper"],"short-title":[],"issued":{"date-parts":[[2016,10,24]]},"references-count":9,"alternative-id":["10.1145\/2993600.2993611","10.1145\/2993600"],"URL":"https:\/\/doi.org\/10.1145\/2993600.2993611","relation":{},"subject":[],"published":{"date-parts":[[2016,10,24]]},"assertion":[{"value":"2016-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}