{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:23:19Z","timestamp":1743067399770,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","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":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_27","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"407-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Quicksort Revisited"],"prefix":"10.1007","author":[{"given":"Razvan","family":"Certezeanu","sequence":"first","affiliation":[]},{"given":"Sophia","family":"Drossopoulou","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Egelund-Muller","sequence":"additional","affiliation":[]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]},{"given":"Sinduran","family":"Sivarajan","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Wheelhouse","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K Apt","year":"2009","unstructured":"Apt, K., Boer, F., Olderog, E.: Verification of Sequential and Concurrent Programs. Springer, Dordrecht (2009)"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 4334. Springer, Heidelberg (2007)"},{"key":"27_CR3","unstructured":"Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Sivarajan, S., Wheelhouse, M., Leino, K.: Dafny Code for Variations on Quicksort. http:\/\/www.doc.ic.ac.uk\/~mjw03\/research\/quicksort.html"},{"key":"27_CR4","unstructured":"Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Sivarajan, S., Wheelhouse, M., Leino, K.:Apollo: An interactive Program and Proof development tool for Java and Haskell, based on Dafny (to appear)"},{"key":"27_CR5","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.: Proof of a recursive program: quicksort. Comput. J. 14, 391\u2013395 (1971)","journal-title":"Comput. J."},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Computer Aided Verification","author":"S de Gouw","year":"2015","unstructured":"de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273\u2013289. Springer, Heidelberg (2015)"},{"key":"27_CR7","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/366622.366644","volume":"4","author":"C Hoare","year":"1961","unstructured":"Hoare, C.: Algorithm 64: quicksort. Commun. ACM 4, 321 (1961)","journal-title":"Commun. ACM"},{"key":"27_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"27_CR9","unstructured":"Lamort, L.:Thinking Above the Code. https:\/\/www.youtube.com\/watch?v=-4Yp3j_jk8Q"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","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-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"27_CR11","unstructured":"Leino, K.: Dafny: An Automatic Program Verifier for Functional Correctness. http:\/\/dafny.codeplex.com"},{"key":"27_CR12","volume-title":"Mathematical Theory of Computation","author":"Z Manna","year":"1974","unstructured":"Manna, Z.: Mathematical Theory of Computation. McGraw-Hill, New York (1974)"},{"key":"27_CR13","unstructured":"Oracle Documentation: Arrays (Java Platform SE 7). http:\/\/docs.oracle.com\/javase\/7\/docs\/api\/java\/util\/Arrays.html"},{"key":"27_CR14","unstructured":"The Verification Corner - Microsoft Research. http:\/\/research.microsoft.com\/en-us\/projects\/verificationcorner"},{"key":"27_CR15","unstructured":"Wikipedia: Quicksort. https:\/\/en.wikipedia.org\/wiki\/Quicksort"},{"key":"27_CR16","unstructured":"YouTube: Quick-sort with Hungarian (Kkllmenti legnyes) folk dance. https:\/\/www.youtube.com\/watch?v=ywWBy6J5gz8"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T12:24:59Z","timestamp":1720787099000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_27"}},"subtitle":["Verifying Alternative Versions of Quicksort"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}