{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:00Z","timestamp":1780994580667,"version":"3.54.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,8,31]],"date-time":"2017-08-31T00:00:00Z","timestamp":1504137600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Open University of The Netherlands"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,1]]},"DOI":"10.1007\/s10817-017-9426-4","type":"journal-article","created":{"date-parts":[[2017,8,31]],"date-time":"2017-08-31T09:24:39Z","timestamp":1504171479000},"page":"93-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["Verifying OpenJDK\u2019s Sort Method for Generic Collections"],"prefix":"10.1007","volume":"62","author":[{"given":"Stijn","family":"de Gouw","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank S.","family":"de Boer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominic","family":"Steinh\u00f6fel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,8,31]]},"reference":[{"key":"9426_CR1","volume-title":"Deductive Software Verification\u2014The KeY Book: From Theory to Practice, LNCS","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P., Ulbrich, M. (eds.): Deductive Software Verification\u2014The KeY Book: From Theory to Practice, LNCS, vol. 10001. Springer, Berlin (2016)"},{"key":"9426_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Mostowski, W., Paganelli, G.: Real-time Java API specifications for high coverage test generation. In: Proceedings of the 10th International Workshop on Java Technologies for Real-Time and Embedded Systems, JTRES \u201912, pp. 145\u2013154. ACM, New York (2012)","DOI":"10.1145\/2388936.2388960"},{"issue":"4","key":"9426_CR3","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1093\/comjnl\/bxp023","volume":"53","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Abdel-Hamid, A.T., Tahar, S., Harrison, J.: Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput. J. 53(4), 465\u2013488 (2010)","journal-title":"Comput. J."},{"issue":"1","key":"9426_CR4","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/MIS.2014.3","volume":"29","author":"B Beckert","year":"2014","unstructured":"Beckert, B., H\u00e4hnle, R.: Reasoning and verification. IEEE Intell. Syst. 29(1), 20\u201329 (2014)","journal-title":"IEEE Intell. Syst."},{"key":"9426_CR5","volume-title":"Proceedings, Software Engineering and Formal Methods (SEFM)","author":"B Beckert","year":"2004","unstructured":"Beckert, B., Klebanov, V.: Proof reuse for deductive program verification. In: Cuellar, J., Liu, Z. (eds.) Proceedings, Software Engineering and Formal Methods (SEFM). IEEE Press, Beijing (2004)"},{"key":"9426_CR6","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference TACAS, London, UK, LNCS","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses (report on SV-COMP 2015). In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference TACAS, London, UK, LNCS, vol. 9035, pp. 401\u2013416. Springer, Berlin (2015)"},{"issue":"1","key":"9426_CR7","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"key":"9426_CR8","unstructured":"Breunesse, C.B.: On JML: Topics in tool-assisted verification of Java programs. Ph.D. Thesis, Radboud University of Nijmegen (2006)"},{"issue":"2","key":"9426_CR9","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"9426_CR10","unstructured":"Filli\u00e2tre, J.C., Magaud, N.: Certification of sorting algorithms in the system Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends. Nice, France (1999). http:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/Filliatre-Magaud.ps.gz"},{"issue":"4","key":"9426_CR11","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1093\/comjnl\/14.4.391","volume":"14","author":"M Foley","year":"1971","unstructured":"Foley, M., Hoare, C.A.R.: Proof of a recursive program: quicksort. Comput. J. 14(4), 391\u2013395 (1971)","journal-title":"Comput. J."},{"issue":"2","key":"9426_CR12","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10817-013-9300-y","volume":"53","author":"S Gouw de","year":"2014","unstructured":"de Gouw, S., de Boer, F.S., Rot, J.: Proof pearl: the KeY to correct and stable sorting. J. Autom. Reason. 53(2), 129\u2013139 (2014)","journal-title":"J. Autom. Reason."},{"key":"9426_CR13","unstructured":"de\u00a0Gouw, S., Rot, J., de\u00a0Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: The good, the bad and the worst case. In: Computer Aided Verification\u201427th International Conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I, pp. 273\u2013289 (2015)"},{"key":"9426_CR14","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., WernerDietl: JML Reference Manual (2013). http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/\/OldReleases\/jmlrefman.pdf . Draft revision 2344"},{"key":"9426_CR15","first-page":"467","volume-title":"Proceedings of the Fourth Annual ACM\/SIGACT-SIAM Symposium on Discrete Algorithms, Austin","author":"PM McIlroy","year":"1993","unstructured":"McIlroy, P.M.: Optimistic sorting and information theoretic complexity. In: Ramachandran, V. (ed.) Proceedings of the Fourth Annual ACM\/SIGACT-SIAM Symposium on Discrete Algorithms, Austin, pp. 467\u2013474. ACM\/SIAM, Philadelphia (1993)"},{"key":"9426_CR16","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-31984-9_27","volume-title":"Proceedings of Fundamental Approaches to Software Engineering (FASE), Edinburgh, LNCS","author":"W Mostowski","year":"2005","unstructured":"Mostowski, W.: Formalisation and verification of Java card security properties in dynamic logic. In: Cerioli, M. (ed.) Proceedings of Fundamental Approaches to Software Engineering (FASE), Edinburgh, LNCS, vol. 3442, pp. 357\u2013371. Springer, Berlin (2005)"},{"key":"9426_CR17","unstructured":"Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) Proceedings of the 4th International Verification Workshop in Connection with CADE-21, Bremen, Germany, CEUR Workshop Proceedings, vol. 259. CEUR-WS.org (2007)"},{"key":"9426_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover, LNCS","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover, LNCS, vol. 828. Springer, Berlin (1994)"},{"key":"9426_CR19","unstructured":"Peters, T.: TimSort description. http:\/\/svn.python.org\/projects\/python\/trunk\/Objects\/listsort.txt . Accessed Feb 2015"},{"key":"9426_CR20","first-page":"414","volume-title":"Formal Methods, 20th International Symposium Oslo, Norway, LNCS","author":"N Polikarpova","year":"2015","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bj\u00f8rner, N., de Boer, F.S. (eds.) Formal Methods, 20th International Symposium Oslo, Norway, LNCS, vol. 9109, pp. 414\u2013434. Springer, Berlin (2015)"},{"key":"9426_CR21","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-57529-4_61","volume-title":"Foundations of Software Technology and Theoretical Computer Science, 13th Conference, Bombay, India, LNCS","author":"W Reif","year":"1993","unstructured":"Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) Foundations of Software Technology and Theoretical Computer Science, 13th Conference, Bombay, India, LNCS, vol. 761, pp. 284\u2013293. Springer, Berlin (1993)"},{"key":"9426_CR22","first-page":"57","volume-title":"Formal Methods and Software Engineering\u201418th International Conference on Formal Engineering Methods (ICFEM), Proceedings, LNCS","author":"D Scheurer","year":"2016","unstructured":"Scheurer, D., H\u00e4hnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) Formal Methods and Software Engineering\u201418th International Conference on Formal Engineering Methods (ICFEM), Proceedings, LNCS, vol. 10009, pp. 57\u201373. Springer, Berlin (2016)"},{"key":"9426_CR23","doi-asserted-by":"crossref","unstructured":"Sforza, F., Batt\u00fa, L., Brunelli, M., Castelnuovo, A., Magnaghi, M.: A \u201cdesign for verification\u201d methodology. In: 2nd International Symposium on Quality of Electronic Design (ISQED), San Jose, CA, USA, pp. 50\u201355. IEEE Computer Society (2001)","DOI":"10.1109\/ISQED.2001.915205"},{"issue":"4","key":"9426_CR24","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 GHC\u2019s mergesort. J. Autom. Reason. 51(4), 357\u2013370 (2013)","journal-title":"J. Autom. Reason."},{"key":"9426_CR25","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: Autoproof: auto-active functional verification of object-oriented programs. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, pp. 566\u2013580. Springer, New York (2015)","DOI":"10.1007\/978-3-662-46681-0_53"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9426-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9426-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9426-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T10:28:51Z","timestamp":1750847331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9426-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,31]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1]]}},"alternative-id":["9426"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9426-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,31]]},"assertion":[{"value":"17 December 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 August 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 August 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}