A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms

Mohsen Safari, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Sorting is one of the fundamental operations in computer science, and many sequential and parallel algorithms have been proposed in the literature. Swap-based sorting algorithms are one category of sorting algorithms where elements are swapped repeatedly to achieve the desired order. Since these algorithms are widely used in practice, their (functional) correctness, i.e., proving sortedness and permutation properties, is of utmost importance. However, proving the permutation property using automated program verifiers is much more challenging as the formal definition of this property involves existential quantifiers. In this paper, we propose a generic pattern to verify the permutation property for any sequential and parallel swap-based sorting algorithm automatically. To demonstrate our approach, we use VerCors, a verification tool based on separation logic for concurrent and parallel programs, to verify the permutation property of bubble sort, selection sort, insertion sort, parallel odd-even transposition sort, quick sort, two in-place merge sorts and TimSort for any arbitrary size of input.
Original languageEnglish
Title of host publicationIntegrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings
EditorsBrijesh Dongol, Elena Troubitsyna
PublisherSpringer
Pages257-275
Number of pages19
ISBN (Electronic)978-3-030-63461-2
ISBN (Print)978-3-030-63460-5
DOIs
Publication statusPublished - 13 Nov 2020
Event16th International Conference on Integrated Formal Methods, IFM 2020 - Virtual Event
Duration: 16 Nov 202020 Nov 2020
Conference number: 16

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12546

Conference

Conference16th International Conference on Integrated Formal Methods, IFM 2020
Abbreviated titleIFM 2020
CityVirtual Event
Period16/11/2020/11/20

Fingerprint

Dive into the research topics of 'A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms'. Together they form a unique fingerprint.

Cite this