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 language | English |
---|---|
Title of host publication | Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings |
Editors | Brijesh Dongol, Elena Troubitsyna |
Publisher | Springer |
Pages | 257-275 |
Number of pages | 19 |
ISBN (Electronic) | 978-3-030-63461-2 |
ISBN (Print) | 978-3-030-63460-5 |
DOIs | |
Publication status | E-pub ahead of print/First online - 13 Nov 2020 |
Event | 16th International Conference on Integrated Formal Methods, IFM 2020 - Virtual Event Duration: 16 Nov 2020 → 20 Nov 2020 Conference number: 16 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 12546 |
Conference
Conference | 16th International Conference on Integrated Formal Methods, IFM 2020 |
---|---|
Abbreviated title | IFM 2020 |
City | Virtual Event |
Period | 16/11/20 → 20/11/20 |
Keywords
- 22/2 OA procedure