{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T23:07:20Z","timestamp":1773788840771,"version":"3.50.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031765537","type":"print"},{"value":"9783031765544","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_3","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:18:05Z","timestamp":1731410285000},"page":"35-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Implementing, Specifying, and\u00a0Verifying the\u00a0QOI Format in\u00a0Dafny: A Case Study"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4082-570X","authenticated-orcid":false,"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8938-4396","authenticated-orcid":false,"given":"Diana-Elena","family":"Gratie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Examples of formal proofs about data compression. In: International Symposium on Information Theory and Its Applications, ISITA 2018, Singapore, October 28\u201331, 2018, pp. 633\u2013637. IEEE (2018). https:\/\/doi.org\/10.23919\/ISITA.2018.8664276","DOI":"10.23919\/ISITA.2018.8664276"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"3_CR3","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). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Bucev, M., Kun\u010dak, V.: Formally verified Quite OK Image Format. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17\u201321, 2022. pp. 343\u2013348. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_41","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_41"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Deutsch, L.P.: DEFLATE Compressed Data Format Specification version 1.3. RFC 1951 (1996). https:\/\/doi.org\/10.17487\/RFC1951, https:\/\/www.rfc-editor.org\/info\/rfc1951","DOI":"10.17487\/RFC1951"},{"key":"3_CR6","unstructured":"Fabien\u00a0Chouteau, J.H.: Quite proved image format. https:\/\/blog.adacore.com\/quite-proved-image-format"},{"key":"3_CR7","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":"3_CR8","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"issue":"4","key":"3_CR9","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/S10817-017-9437-1","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Refinement to Imperative HOL. J. Autom. Reason. 62(4), 481\u2013503 (2019). https:\/\/doi.org\/10.1007\/S10817-017-9437-1","journal-title":"J. Autom. Reason."},{"key":"3_CR10","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). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-54108-7_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"KRM Leino","year":"2014","unstructured":"Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 170\u2013190. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_9"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol.\u00a02283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"3_CR14","unstructured":"Senjak, C., Hofmann, M.: An implementation of Deflate in Coq. CoRR abs\/1609.01220 (2016). http:\/\/arxiv.org\/abs\/1609.01220"},{"key":"3_CR15","unstructured":"Szablewski, D.: QOI - the \u201cQuite OK Image Format\u201d for fast, lossless image compression. https:\/\/github.com\/phoboslab\/qoi"},{"key":"3_CR16","unstructured":"Szablewski, D.: The Quite OK Image Format specification. https:\/\/qoiformat.org\/qoi-specification.pdf"},{"key":"3_CR17","unstructured":"The Coq Development Team: The Coq reference manual \u2013 release 8.19.0 (2024). https:\/\/coq.inria.fr\/doc\/V8.19.0\/refman"},{"key":"3_CR18","unstructured":"The dafny-lang community: Dafny reference manual (2024). https:\/\/dafny.org\/dafny\/DafnyRef\/DafnyRef"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Ye, Q., Delaware, B.: A verified protocol buffer compiler. In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14\u201315, 2019. pp. 222\u2013233. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294105","DOI":"10.1145\/3293880.3294105"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:10Z","timestamp":1737200290000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}