Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
VSTTE, 2017, Vol.10712, p.35-48
2017

Details

Autor(en) / Beteiligte
Titel
Proving JDK's Dual Pivot Quicksort Correct
Ist Teil von
  • VSTTE, 2017, Vol.10712, p.35-48
Ort / Verlag
Switzerland: Springer International Publishing AG
Erscheinungsjahr
2017
Link zum Volltext
Quelle
Alma/SFX Local Collection
Beschreibungen/Notizen
  • Sorting is a fundamental functionality in libraries, for which efficiency is crucial. Correctness of the highly optimised implementations is often taken for granted. De Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit (JDK) implementation of TimSort. We have formally analysed the other implementation of sorting in the JDK standard library: A highly efficient implementation of a dual pivot quicksort algorithm. We were able to deductively prove that the algorithm implementation is correct. However, a loop invariant which is annotated to the source code does not hold. This paper reports on how an existing piece of non-trivial Java software can be made accessible to deductive verification and successfully proved correct, for which we use the Java verification engine KeY.
Sprache
Englisch
Identifikatoren
ISBN: 9783319723075, 3319723073, 9783319723082, 3319723081
ISSN: 0302-9743
eISSN: 1611-3349
DOI: 10.1007/978-3-319-72308-2_3
Titel-ID: cdi_springer_books_10_1007_978_3_319_72308_2_3

Weiterführende Literatur

Empfehlungen zum selben Thema automatisch vorgeschlagen von bX