{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T11:16:16Z","timestamp":1762254976702,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031690419"},{"type":"electronic","value":"9783031690426"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-69042-6_3","type":"book-chapter","created":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T14:46:52Z","timestamp":1724770012000},"page":"38-56","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Certification of\u00a0Sorting Algorithms Using Theorema and\u00a0Coq"],"prefix":"10.1007","author":[{"given":"Isabela","family":"Dr\u0103mnesc","sequence":"first","affiliation":[]},{"given":"Tudor","family":"Jebelean","sequence":"additional","affiliation":[]},{"given":"Sorin","family":"Stratulat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,28]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P., Ulbrich, M.: Deductive Software Verification. The KeY Book: From Theory to Practice. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Baity, R., Humphrey, L.R., Hopkinson, K.: Formal verification of a merge sort algorithm in SPARK. In: AIAA SciTech Forum, American Institute of Aeronautics and Astronautics (2024\/02\/01) (2021). https:\/\/doi.org\/10.2514\/6.2021-0039","DOI":"10.2514\/6.2021-0039"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-72308-2_3","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"B Beckert","year":"2017","unstructured":"Beckert, B., Schiffl, J., Schmitt, P.H., Ulbrich, M.: Proving JDK\u2019s dual pivot quicksort correct. In: Paskevich, A., Wies, T. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 35\u201348. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_3"},{"key":"3_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, vol","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, vol. Springer, XXV (2004)"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Bockenek, J., Lammich, P., Nemouchi, Y., Wolff, B.: Using Isabelle\/UTP for the verification of sorting algorithms: A case study. EasyChair Preprint no. 944 (2019). https:\/\/doi.org\/10.29007\/ddqm","DOI":"10.29007\/ddqm"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11617990_6","volume-title":"Types for Proofs and Programs","author":"A Bove","year":"2006","unstructured":"Bove, A., Coquand, T.: Formalising bitonic sort in type theory. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) Types for Proofs and Programs, pp. 82\u201397. Springer Berlin Heidelberg, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11617990_6"},{"key":"3_CR7","unstructured":"Buchberger, B.: Algorithm invention and verification by lazy thinking. In: Analele Universitatii de Vest, Timisoara, Ser. Matematica - Informatica. vol.\u00a0XLI, pp. 41\u201370 (2003)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Buchberger, B., Jebelean, T., Kriftner, F., Marin, M., Tomuta, E., Vasaru, D.: A survey on the Theorema project. In: International Symposium on Symbolic and Algebraic Computation, pp. 384\u2013391. ACM Press (1997)","DOI":"10.1145\/258726.258853"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: Computer-assisted natural-style mathematics. J. Formalized Reason. 9(1), 149\u2013185 (2016).https:\/\/doi.org\/10.6092\/issn.1972-5787\/4568","DOI":"10.6092\/issn.1972-5787\/4568"},{"key":"3_CR10","unstructured":"Burgos, M.P.F.: Formalization of sorting algorithms in Isabelle\/HOL. Master\u2019s thesis, Vrije Universiteit Amsterdam (2019)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Leino, K.R.M., Sivarajan, S., Wheelhouse, M.: Quicksort revisited: Verifying alternative versions of quicksort. Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pp. 407\u2013426 (2016)","DOI":"10.1007\/978-3-319-30734-3_27"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Couturier, R.: Formal engineering of the bitonic sort using PVS. In: Proceedings of the 2nd Irish Conference on Formal Methods (IW-FM\u201998), pp. 16\u201334. BCS Learning & Development Ltd., Swindon, GBR (1998)","DOI":"10.14236\/ewic\/FM1998.2"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jsc.2014.09.030","volume":"68","author":"I Dramnesc","year":"2015","unstructured":"Dramnesc, I., Jebelean, T.: Synthesis of list algorithms by mechanical proving. J. Symb. Comput. 68, 61\u201392 (2015). https:\/\/doi.org\/10.1016\/j.jsc.2014.09.030","journal-title":"J. Symb. Comput."},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-030-43120-4_13","volume-title":"Mathematical Aspects of Computer and Information Sciences: 8th International Conference, MACIS 2019, Gebze, Turkey, November 13\u201315, 2019, Revised Selected Papers","author":"I Dr\u0103mnesc","year":"2020","unstructured":"Dr\u0103mnesc, I., Jebelean, T.: Automatic synthesis of merging and inserting algorithms on binary trees using multisets in Theorema. In: Slamanig, D., Tsigaridas, E., Zafeirakopoulos, Z. (eds.) Mathematical Aspects of Computer and Information Sciences: 8th International Conference, MACIS 2019, Gebze, Turkey, November 13\u201315, 2019, Revised Selected Papers, pp. 153\u2013168. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43120-4_13"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Dramnesc, I., Jebelean, T.: Synthesis of sorting algorithms using multisets in Theorema. J. Logical Algebraic Methods Programm. 119, 100635 (2020). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100635","DOI":"10.1016\/j.jlamp.2020.100635"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-030-85315-0_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2021: 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8\u201310, 2021, Proceedings","author":"I Dr\u0103mnesc","year":"2021","unstructured":"Dr\u0103mnesc, I., Jebelean, T.: AlCons\u202f: deductive synthesis of sorting algorithms in Theorema. In: Cerone, A., \u00d6lveczky, P.C. (eds.) Theoretical Aspects of Computing \u2013 ICTAC 2021: 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8\u201310, 2021, Proceedings, pp. 314\u2013333. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_18"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Dramnesc, I., Jebelean, T.: Mechanical verification of insert-sort and merge-sort using multisets in Theorema. In: IEEE 21st International Symposium on Intelligent Systems and Informatics (SISY 2023), pp. 55\u201360. IEEE Xplore (2023)","DOI":"10.1109\/SISY60376.2023.10417933"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jsc.2018.04.002","volume":"90","author":"I Dramnesc","year":"2019","unstructured":"Dramnesc, I., Jebelean, T., Stratulat, S.: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. J. Symb. Comput. 90, 3\u201341 (2019)","journal-title":"J. Symb. Comput."},{"key":"3_CR19","unstructured":"Filli\u00e2tre, J.C., Magaud, N.: Certification of sorting algorithms in the system Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends (1999)"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Georgiou, P., Hajdu, M., Kovacs, L.: Saturating sorting without sorts. In: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024). EPiC Series in Computing, vol.\u00a0100, pp. 88\u2013105. EasyChair (2024).https:\/\/doi.org\/10.29007\/rg9z, https:\/\/easychair.org\/publications\/paper\/qbDc","DOI":"10.29007\/rg9z"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"de\u00a0Gouw, S., de\u00a0Boer, F.S., Rot, J.: Verification of counting sort and radix sort. Deductive Software Verification\u2013The KeY Book: From Theory to Practice, pp. 609\u2013618 (2016)","DOI":"10.1007\/978-3-319-49812-6_19"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: Spark 2014 and GNATprove. Int. J. Softw. Tools Technol. Transfer 17(6), 695\u2013707 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0322-5","DOI":"10.1007\/s10009-014-0322-5"},{"key":"3_CR23","unstructured":"Howard, W.A.: The formulas-as-types notion of construction. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479\u2013490. Academic Press (1980), reprint of 1969 article"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Jiang, D., Zhou, M.: A comparative study of insertion sorting algorithm verification. In: 2017 IEEE 2nd Information Technology, Networking, Electronic and Automation Control Conference (ITNEC), pp. 321\u2013325 (2017). https:\/\/doi.org\/10.1109\/ITNEC.2017.8284998","DOI":"10.1109\/ITNEC.2017.8284998"},{"key":"3_CR25","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 Version 8.3 - The User\u2019s Manual (1999)"},{"key":"3_CR26","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 3: Sorting and Searching, 2nd edn. Addison Wesley (1998)"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Logic Algebraic Programm. 58(1-2), 89\u2013106 (2004). https:\/\/doi.org\/10.1016\/j.jlap.2003.07.006, https:\/\/hal.science\/hal-01984932","DOI":"10.1016\/j.jlap.2003.07.006"},{"volume-title":"Isabelle\/HOL","year":"2002","key":"3_CR28","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. Springer Berlin Heidelberg, Berlin, Heidelberg (2002)"},{"key":"3_CR29","unstructured":"Petrovic, D.: Verification of selection and heap sort using locales. Arch. Formal Proofs (2014). https:\/\/www.isa-afp.org\/entries\/Selection_Heap_Sort.shtml"},{"key":"3_CR30","unstructured":"Quarfot\u00a0Orrevall, S., Gengelbach, A.: Implementation and verification of sorting algorithms with the interactive theorem prover HOL. Student thesis, Department of Information Technology, Mathematics and Computer Science, Disciplinary Domain of Science and Technology, Uppsala University (2020). http:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:uu:diva-424295"},{"key":"3_CR31","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-030-63461-2_14","volume-title":"Integrated Formal Methods: 16th International Conference, IFM 2020, Lugano, Switzerland, November 16\u201320, 2020, Proceedings","author":"M Safari","year":"2020","unstructured":"Safari, M., Huisman, M.: A generic approach to the verification of the permutation property of sequential and parallel swap-based sorting algorithms. In: Dongol, B., Troubitsyna, E. (eds.) Integrated Formal Methods: 16th International Conference, IFM 2020, Lugano, Switzerland, November 16\u201320, 2020, Proceedings, pp. 257\u2013275. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_14"},{"key":"3_CR32","unstructured":"Sandip, R., Sumners, R.W.: Verification of an in-place quicksort in ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (2002). https:\/\/api.semanticscholar.org\/CorpusID:264243016"},{"key":"3_CR33","unstructured":"Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS prover guide - version 7.1. SRI International (2020)"},{"issue":"4","key":"3_CR34","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10817-012-9260-7","volume":"51","author":"C Sternagel","year":"2013","unstructured":"Sternagel, C.: Proof pearl - a mechanized proof of GHCs mergesort. J. Autom. Reason. 51(4), 357\u2013370 (2013)","journal-title":"J. Autom. Reason."},{"key":"3_CR35","unstructured":"The Coq development team: The Coq Reference Manual. INRIA (2020). http:\/\/coq.inria.fr\/doc"},{"key":"3_CR36","unstructured":"Tushkanova, E., Giorgetti, A., Kouchnarenko, O.: Specifying and proving a sorting algorithm. Tech. rep., Laboratoire d\u2019Informatique de l\u2019Universit\u00e9 de Franche-Comte (2009)"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Windsteiger, W.: Theorema 2.0: A system for mathematical theory exploration. In: ICMS 2014. LNCS, vol.\u00a08592, pp. 49\u201352 (2014). https:\/\/doi.org\/10.1007\/978-3-662-44199-2_9","DOI":"10.1007\/978-3-662-44199-2_9"},{"key":"3_CR38","unstructured":"Zhang, Y., Zhao, Y., Sanan, D.: A verified timsort C implementation in Isabelle\/HOL. arXiv preprint arXiv:1812.03318 (2018)"}],"container-title":["Lecture Notes in Computer Science","Symbolic Computation in Software Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-69042-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T14:47:38Z","timestamp":1724770058000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-69042-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031690419","9783031690426"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-69042-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"28 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SCSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Symbolic Computation in Software Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"28 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sycss2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/scss-conference.org\/2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}