{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:18:14Z","timestamp":1746159494743,"version":"3.40.4"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031866944","type":"print"},{"value":"9783031866951","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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-86695-1_3","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:45Z","timestamp":1746151605000},"page":"28-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deductive Verification of\u00a0Sparse Sets in\u00a0Why3"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9477-8109","authenticated-orcid":false,"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Assigning Programs to Meanings (1996)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"3_CR3","volume-title":"The Design and Analysis of Computer Algorithms","author":"AV Aho","year":"1974","unstructured":"Aho, A.V., Hopcroft, J.E.: The Design and Analysis of Computer Algorithms, 1st edn. Addison-Wesley Longman Publishing Co., Inc, USA (1974)","edition":"1"},{"issue":"1\u20134","key":"3_CR4","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1145\/176454.176484","volume":"2","author":"P Briggs","year":"1993","unstructured":"Briggs, P., Torczon, L.: An efficient representation for sparse sets. LOPLAS 2(1\u20134), 59\u201369 (1993)","journal-title":"LOPLAS"},{"key":"3_CR5","unstructured":"Brisset, P., Barnier, N.: FaCiLe\u202f: a functional constraint library. In: CICLOPS: Colloquium on Implementation of Constraint and LOgic Programming Systems, p. 2001. Paphos, Cyprus (2001)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: A certified constraint solver over finite domains. In: Formal Methods (FM 2012). volume 7436 of LNCS, pp. 116\u2013131. France, Paris (2012)","DOI":"10.1007\/978-3-642-32759-9_12"},{"key":"3_CR7","unstructured":"Cristi\u00e1, M.,\u00a0Dubois, C.: Comparing EventB, log and why3 models of sparse sets. In: 35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2024). Saint-Jacut-de-la-Mer, France (2024)"},{"key":"3_CR8","unstructured":"Cristi\u00e1, M.,\u00a0Rossi, G.: $$\\{\\mathit{log}\\}$$: set formulas as programs. Rend. Ist. Mat. Univ. Trieste 53, 24 (2021)"},{"key":"3_CR9","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 version of the sparse arrays example, the first example of the vacid-0 benchmarks. https:\/\/toccata.gitlabpages.inria.fr\/toccata\/gallery\/vacid_0_sparse_array.en.html"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C.,\u00a0Paskevich, A.: Why3 - where programs meet provers. In:\u00a0Felleisen. M.,\u00a0Gardner, P. (eds.) 22nd European Symposium on Programming, ESOP 2013, Held as Part of ETAPS 2013, Rome, Italy, Proceedings, volume 7792 of LNCS, pp. 125\u2013128. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C.,\u00a0Paskevich A.: Abstraction and genericity in why3. In:\u00a0Margaria, T.,\u00a0Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part I, volume 12476 of Lecture Notes in Computer Science, pp. 122\u2013142. Springer (2020)","DOI":"10.1007\/978-3-030-61362-4_7"},{"key":"3_CR12","volume-title":"Specifying Systems","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Addison-Wesley, The TLA+ Language and Tools for Hardware and Software Engineers (2002)"},{"key":"3_CR13","unstructured":"Le Cl\u00e9ment de Saint-Marcq, V.,\u00a0Schaus, P.,\u00a0Solnon, C.,\u00a0Lecoutre C.: Sparse-Sets for domain implementation. In: CP workshop on Techniques foR Implementing Constraint programming Systems (TRICS), pp. 1\u201310 (2013)"},{"key":"3_CR14","unstructured":"Ledein A.,\u00a0Dubois, C.: Facile en coq : v\u00e9rification formelle des listes d\u2019intervalles. In: 31\u00e8me Journ\u00e9es Francophones des Langages Applicatifs (2019)"},{"key":"3_CR15","unstructured":"Leino, K.R.M.,\u00a0Moskal, M.: Vacid-0: verification of ample correctness of invariants of data-structures, edition 0. In: Proceedings of Tools and Experiments Workshop at VSTTE (2010)"},{"issue":"1","key":"3_CR16","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s12532-020-00190-7","volume":"13","author":"L Michel","year":"2021","unstructured":"Michel, L., Schaus, P., Van Hentenryck, P.: Minicp: a lightweight solver for constraint programming. Math. Program. Comput. 13(1), 133\u2013184 (2021)","journal-title":"Math. Program. Comput."},{"key":"3_CR17","unstructured":"Schaus, P., Landtsheer, R.D.: Oscar user-guide (2016). http:\/\/oscarlib.org"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Schwartz, J.T., Dewar, R.B.K.,\u00a0Dubinsky, E.,\u00a0Schonberg, E.: Programming with Sets - An Introduction to SETL. Texts and Monographs in Computer Science. Springer (1986)","DOI":"10.1007\/978-1-4613-9575-1"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-86695-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:55Z","timestamp":1746151615000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-86695-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031866944","9783031866951"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-86695-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"3 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","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":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.soundandcomplete.org\/vstte2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}