Verification of dual pivot quicksort program

Результат исследования: Научные публикации в периодических изданияхстатья по материалам конференции

Аннотация

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.

Язык оригиналаанглийский
Страницы (с-по)511-524
Число страниц14
ЖурналCEUR Workshop Proceedings
Том2260
DOI
СостояниеОпубликовано - 1 янв 2018
Событие20th Conference Scientific Services and Internet, SSI 2018 - Novorossiysk-Abrau, Российская Федерация
Продолжительность: 17 сен 201822 сен 2018

Fingerprint Подробные сведения о темах исследования «Verification of dual pivot quicksort program». Вместе они формируют уникальный семантический отпечаток (fingerprint).

Цитировать