{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T13:15:33Z","timestamp":1720790133758},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10817-013-9300-y","type":"journal-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T11:02:14Z","timestamp":1389697334000},"page":"129-139","source":"Crossref","is-referenced-by-count":11,"title":["Proof Pearl: The KeY to Correct and Stable Sorting"],"prefix":"10.1007","volume":"53","author":[{"given":"Stijn","family":"de Gouw","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"de Boer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"9300_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 \u201912, pp. 145\u2013154. ACM, New York (2012). doi: 10.1145\/2388936.2388960","DOI":"10.1145\/2388936.2388960"},{"key":"9300_CR2","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd Edn. Texts in Computer Science. Springer-Verlag (2009). 502 pp, ISBN 978-1-84882-744-8"},{"issue":"3","key":"9300_CR3","doi-asserted-by":"crossref","first-page":"823","DOI":"10.1016\/j.jcss.2011.08.002","volume":"78","author":"KR Apt","year":"2012","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R., de Gouw, S.: Verification of Object-Oriented programs: A transformational approach. J. Comput. Syst. Sci. 78(3), 823\u2013852 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"9300_CR4","unstructured":"Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Secure information flow for Java. A Dynamic Logic approach. Karlsruhe reports in informatics; 2013-10, KIT (2013). http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000036786"},{"key":"9300_CR5","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach, Lecture Notes in Computer Science, vol. 4334. Springer (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"issue":"3","key":"9300_CR6","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transfer 7(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9300_CR7","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":"9300_CR8","doi-asserted-by":"crossref","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":"9300_CR9","unstructured":"Mostowski, W.: Formalisation and verification of Java Card security properties in Dynamic Logic. In: M. Cerioli (ed.) Proceedings Fundamental Approaches to Software Engineering (FASE), Edinburgh, Lecture Notes in Computer Science, vol. 3442, pp. 357\u2013371. Springer (2005). http:\/\/www.springerlink.com\/link.asp?id=x0u5bj47bcqhy4b7"},{"key":"9300_CR10","unstructured":"Mostowski, W.: Fully verified Java Card API reference implementation. In: VERIFY (2007)"},{"issue":"4","key":"9300_CR11","doi-asserted-by":"crossref","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":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9300-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9300-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9300-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T09:44:07Z","timestamp":1565084647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9300-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,15]]},"references-count":11,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["9300"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9300-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1,15]]}}}