Verification of dual pivot quicksort program

Research output: Contribution to journalConference articlepeer-review


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.

Original languageEnglish
Pages (from-to)511-524
Number of pages14
JournalCEUR Workshop Proceedings
Publication statusPublished - 1 Jan 2018
Event20th Conference Scientific Services and Internet, SSI 2018 - Novorossiysk-Abrau, Russian Federation
Duration: 17 Sep 201822 Sep 2018


  • Deductive verification
  • Dual pivot quicksort
  • PVS
  • SMT solver


Dive into the research topics of 'Verification of dual pivot quicksort program'. Together they form a unique fingerprint.

Cite this