{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:37:34Z","timestamp":1742960254933,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"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_24","type":"book-chapter","created":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T20:03:45Z","timestamp":1597262625000},"page":"325-336","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Call Me Back, I Have a Type Invariant"],"prefix":"10.1007","author":[{"given":"M. Anthony","family":"Aiello","sequence":"first","affiliation":[]},{"given":"Johannes","family":"Kanig","sequence":"additional","affiliation":[]},{"given":"Taro","family":"Kurita","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,13]]},"reference":[{"key":"24_CR1","unstructured":"Barnes, J.: Ada 2012 rationale (2012). https:\/\/www.adacore.com\/papers\/ada-2012-rationale\/"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"2004","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3, 2004 (2004)","journal-title":"J. Object Technol."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS 2016, pp. 91\u201396. ACM, New York (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"24_CR4","unstructured":"Charlet, A.: Adacore techdays - GNAT pro update (2018). https:\/\/www.adacore.com\/uploads\/page_content\/presentations\/TechDaysParis2018-2-GNAT-Pro-Update-Tech-Days-2018-Paris.pptx"},{"key":"24_CR5","unstructured":"Daian, P.: Analysis of the DAO exploit (2016). http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/"},{"key":"24_CR6","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 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"24_CR7","unstructured":"Foundation, E.: Solidity (2019). https:\/\/solidity.readthedocs.io\/en\/develop\/"},{"key":"24_CR8","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.M.: Design Patterns: Elements of Reusable Object-Oriented Software, 1st edn. Addison-Wesley Professional, Boston (1994)","edition":"1"},{"issue":"POPL","key":"24_CR9","first-page":"48:1","volume":"2","author":"S Grossman","year":"2017","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2(POPL), 48:1\u201348:28 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"24_CR10","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, 18\u201321 February 2018. The Internet Society (2018). http:\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/25\/2018\/02\/ndss2018_09-1_Kalra_paper.pdf"},{"key":"24_CR11","unstructured":"Kothapalli, A.: Solidify, an LLVM pass to compile LLVM IR into solidity, version 00, July 2017. https:\/\/www.osti.gov\/\/servlets\/purl\/1369636"},{"key":"24_CR12","unstructured":"Leavens, G.T.: JML reference manual (2019). http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/jmlrefman\/jmlrefman_toc.html"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/11526841_4","volume-title":"FM 2005: Formal Methods","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M., M\u00fcller, P.: Modular verification of static class invariants. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 26\u201342. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11526841_4"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, Edmund M., Voronkov, Andrei (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 . https:\/\/www.microsoft.com\/en-us\/research\/publication\/dafny-automatic-program-verifier-functional-correctness-2\/","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"24_CR15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139629294","volume-title":"Building High Integrity Applications with SPARK","author":"JW McCormick","year":"2015","unstructured":"McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)"},{"key":"24_CR16","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Nehai, Z., Bobot, F.: Deductive Proof of Ethereum Smart Contracts Using Why3. Research report, CEA DILS, April 2019. https:\/\/hal.archives-ouvertes.fr\/hal-02108987","DOI":"10.1007\/978-3-030-54994-7_22"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997)","DOI":"10.5210\/fm.v2i9.548"}],"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_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,28]],"date-time":"2021-03-28T08:16:30Z","timestamp":1616919390000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-54994-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030549930","9783030549947"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54994-7_24","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)"}}]}}