Standard

Verification of dual pivot quicksort program. / Shelekhov, V. I.; Сhushkin, M. S.

In: CEUR Workshop Proceedings, Vol. 2260, 01.01.2018, p. 511-524.

Research output: Contribution to journal › Conference article › peer-review

Harvard

Shelekhov, VI & Сhushkin, MS 2018, 'Verification of dual pivot quicksort program', CEUR Workshop Proceedings, vol. 2260, pp. 511-524. https://doi.org/10.20948/abrau-2018-13

APA

Shelekhov, V. I., & Сhushkin, M. S. (2018). Verification of dual pivot quicksort program. CEUR Workshop Proceedings, 2260, 511-524. https://doi.org/10.20948/abrau-2018-13

Vancouver

Shelekhov VI, Сhushkin MS. Verification of dual pivot quicksort program. CEUR Workshop Proceedings. 2018 Jan 1;2260:511-524. doi: 10.20948/abrau-2018-13

Author

Shelekhov, V. I. ; Сhushkin, M. S. / Verification of dual pivot quicksort program. In: CEUR Workshop Proceedings. 2018 ; Vol. 2260. pp. 511-524.

BibTeX

@article{f70d9d07d8b1440b841d369ad0189b4b,
title = "Verification of dual pivot quicksort program",
abstract = "A dual pivot quicksort (DPQS) algorithm performs substantially better than other sorting algorithms in the Java Development Kit (JDK). Beckert B. et al. had constructed the specification of the DPQS algorithm in the JML language. It had been successfully proved correct using the deductive verification engine KeY. Predicate programming has the essential advantages against imperative programming. Deductive verification of a predicate program is approximately 4 times faster than deductive verification of the analogous imperative program. Application of the special optimizing transformations to a predicate program results in the equivalent effective imperative program compared in efficiency with manually programmed. In the current paper, the construction and deductive verification of the DPQS predicate program using the interactive prover PVS is described. Deductive verification of the DPQS predicate program has been made within a week. An effective Java program has been obtained by applying program transformations to the DPQS predicate program. It's comparison with the DPQS algorithm in the JDK is in our plans.",
keywords = "Deductive verification, Dual pivot quicksort, PVS, SMT solver",
author = "Shelekhov, {V. I.} and Сhushkin, {M. S.}",
year = "2018",
month = jan,
day = "1",
doi = "10.20948/abrau-2018-13",
language = "English",
volume = "2260",
pages = "511--524",
journal = "CEUR Workshop Proceedings",
issn = "1613-0073",
publisher = "CEUR-WS",
note = "20th Conference Scientific Services and Internet, SSI 2018 ; Conference date: 17-09-2018 Through 22-09-2018",

}

RIS

TY - JOUR

T1 - Verification of dual pivot quicksort program

AU - Shelekhov, V. I.

AU - Сhushkin, M. S.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - A dual pivot quicksort (DPQS) algorithm performs substantially better than other sorting algorithms in the Java Development Kit (JDK). Beckert B. et al. had constructed the specification of the DPQS algorithm in the JML language. It had been successfully proved correct using the deductive verification engine KeY. Predicate programming has the essential advantages against imperative programming. Deductive verification of a predicate program is approximately 4 times faster than deductive verification of the analogous imperative program. Application of the special optimizing transformations to a predicate program results in the equivalent effective imperative program compared in efficiency with manually programmed. In the current paper, the construction and deductive verification of the DPQS predicate program using the interactive prover PVS is described. Deductive verification of the DPQS predicate program has been made within a week. An effective Java program has been obtained by applying program transformations to the DPQS predicate program. It's comparison with the DPQS algorithm in the JDK is in our plans.

AB - A dual pivot quicksort (DPQS) algorithm performs substantially better than other sorting algorithms in the Java Development Kit (JDK). Beckert B. et al. had constructed the specification of the DPQS algorithm in the JML language. It had been successfully proved correct using the deductive verification engine KeY. Predicate programming has the essential advantages against imperative programming. Deductive verification of a predicate program is approximately 4 times faster than deductive verification of the analogous imperative program. Application of the special optimizing transformations to a predicate program results in the equivalent effective imperative program compared in efficiency with manually programmed. In the current paper, the construction and deductive verification of the DPQS predicate program using the interactive prover PVS is described. Deductive verification of the DPQS predicate program has been made within a week. An effective Java program has been obtained by applying program transformations to the DPQS predicate program. It's comparison with the DPQS algorithm in the JDK is in our plans.

KW - Deductive verification

KW - Dual pivot quicksort

KW - PVS

KW - SMT solver

UR - http://www.scopus.com/inward/record.url?scp=85058157419&partnerID=8YFLogxK

U2 - 10.20948/abrau-2018-13

DO - 10.20948/abrau-2018-13

M3 - Conference article

AN - SCOPUS:85058157419

VL - 2260

SP - 511

EP - 524

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

SN - 1613-0073

T2 - 20th Conference Scientific Services and Internet, SSI 2018

Y2 - 17 September 2018 through 22 September 2018

ER -

ID: 18200475