{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T05:06:48Z","timestamp":1771045608503,"version":"3.50.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_16","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"273-289","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":55,"title":["OpenJDK\u2019s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case"],"prefix":"10.1007","author":[{"given":"Stijn","family":"de Gouw","sequence":"first","affiliation":[]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[]},{"given":"Frank S.","family":"de Boer","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"16_CR1","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 2012, pp. 145\u2013154. ACM, New York (2012)","DOI":"10.1145\/2388936.2388960"},{"issue":"4","key":"16_CR2","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":"16_CR3","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":"16_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","first-page":"120","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"M Pelevina","year":"2014","unstructured":"Pelevina, M., Bubel, R., H\u00e4hnle, R.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 120\u2013134. Springer, Heidelberg (2014)"},{"issue":"2","key":"16_CR6","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. Reasoning 53(2), 129\u2013139 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR7","unstructured":"de Gouw, S., et al: Web appendix of this paper. \n                      http:\/\/envisage-project.eu\/?page_id=1412\n                      \n                     (2015)"},{"key":"16_CR8","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 (1999)"},{"issue":"4","key":"16_CR9","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."},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-642-38574-2_21","volume-title":"Automated Deduction \u2013 CADE-24","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 300\u2013314. Springer, Heidelberg (2013)"},{"key":"16_CR11","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.:. JML Reference Manual, Draft revision 2344 (2013)"},{"key":"16_CR12","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, pp. 467\u2013474. ACM\/SIAM, Austin (1993)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-31984-9_27","volume-title":"Fundamental Approaches to Software Engineering","author":"W Mostowski","year":"2005","unstructured":"Mostowski, W.: Formalisation and verification of Java Card security properties in dynamic logic. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 357\u2013371. Springer, Heidelberg (2005)"},{"key":"16_CR14","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, CEUR Workshop Proceedings, Vol. 259, CEUR-WS.org, Bremen (2007)"},{"key":"16_CR15","unstructured":"Peters, T.: Timsort description. \n                      http:\/\/svn.python.org\/projects\/python\/trunk\/Objects\/listsort.txt\n                      \n                    . Accessed Feb 2015"},{"issue":"4","key":"16_CR16","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. Reasoning 51(4), 357\u2013370 (2013)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:06:34Z","timestamp":1563825994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}