@inproceedings{6eeab50f65fe4d19ba70c113f073785d,
title = "A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms",
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.",
author = "Mohsen Safari and Marieke Huisman",
year = "2020",
month = nov,
day = "13",
doi = "10.1007/978-3-030-63461-2_14",
language = "English",
isbn = "978-3-030-63460-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Singapore",
pages = "257--275",
editor = "Brijesh Dongol and Elena Troubitsyna",
booktitle = "Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings",
address = "Singapore",
note = "16th International Conference on Integrated Formal Methods, IFM 2020, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020",
url = {https://doi.org/10.1007/978-3-030-63461-2_14}
}

{"_id":"CckeBShifXLfh4J7q","bibbaseid":"safari-huisman-agenericapproachtotheverificationofthepermutationpropertyofsequentialandparallelswapbasedsortingalgorithms-2020","authorIDs":[],"author_short":["Safari, M.","Huisman, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms","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.","author":[{"firstnames":["Mohsen"],"propositions":[],"lastnames":["Safari"],"suffixes":[]},{"firstnames":["Marieke"],"propositions":[],"lastnames":["Huisman"],"suffixes":[]}],"year":"2020","month":"November","day":"13","doi":"10.1007/978-3-030-63461-2_14","language":"English","isbn":"978-3-030-63460-5","series":"Lecture Notes in Computer Science","publisher":"Springer Singapore","pages":"257–275","editor":[{"firstnames":["Brijesh"],"propositions":[],"lastnames":["Dongol"],"suffixes":[]},{"firstnames":["Elena"],"propositions":[],"lastnames":["Troubitsyna"],"suffixes":[]}],"booktitle":"Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings","address":"Singapore","note":"16th International Conference on Integrated Formal Methods, IFM 2020, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020","url":"https://doi.org/10.1007/978-3-030-63461-2_14","bibtex":"@inproceedings{6eeab50f65fe4d19ba70c113f073785d,\ntitle = \"A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms\",\nabstract = \"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.\",\nauthor = \"Mohsen Safari and Marieke Huisman\",\nyear = \"2020\",\nmonth = nov,\nday = \"13\",\ndoi = \"10.1007/978-3-030-63461-2_14\",\nlanguage = \"English\",\nisbn = \"978-3-030-63460-5\",\nseries = \"Lecture Notes in Computer Science\",\npublisher = \"Springer Singapore\",\npages = \"257--275\",\neditor = \"Brijesh Dongol and Elena Troubitsyna\",\nbooktitle = \"Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings\",\naddress = \"Singapore\",\nnote = \"16th International Conference on Integrated Formal Methods, IFM 2020, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020\",\nurl = {https://doi.org/10.1007/978-3-030-63461-2_14}\n}\n\n\n","author_short":["Safari, M.","Huisman, M."],"editor_short":["Dongol, B.","Troubitsyna, E."],"key":"6eeab50f65fe4d19ba70c113f073785d","id":"6eeab50f65fe4d19ba70c113f073785d","bibbaseid":"safari-huisman-agenericapproachtotheverificationofthepermutationpropertyofsequentialandparallelswapbasedsortingalgorithms-2020","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-030-63461-2_14"},"metadata":{"authorlinks":{}},"downloads":1,"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2021-03-09T09:25:27.688Z","downloads":1,"keywords":[],"search_terms":["generic","approach","verification","permutation","property","sequential","parallel","swap","based","sorting","algorithms","safari","huisman"],"title":"A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms","year":2020,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}