Formal engineering of the bitonic sort using PVS

Abstract

In this paper, we present a proof that the bitonic sort is sound using PVS, a powerful specification and verification environment. First, we briefly introduce this well-known parallel sort. It is based on bitonic lists whose relevant properties can be proven with PVS. To achieve our goal of constructing the proof from scratch, we start by studying some examples of this sort. Then we try to prove properties of this algorithm. Failure in the proof of particular lemmas provides us with information which helps to correct these lemmas. To complete this proof, we start with general cases, continue by examining each of the exception cases, and finish when all cases have been considered. Then we can construct the specification of the bitonic sort which can easily be translated into a traditional imperative language.

Contributors

Raphaël Couturier

Conference

Publication date: July 1998

Publication date (Print): July 1998

Pages: 1-19

Affiliations

LORIA - UMR n°7503 - CNRS, Université Henri Poincaré

BP 239, 54506 Vandœuvre-lés-Nancy, France

Article

DOI: 10.14236/ewic/FM1998.2

Copyright statement: © Raphaël Couturier. Published by BCS Learning and Development Ltd. 2nd Irish Workshop on Formal Methods, Cork, Ireland

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: 2nd Irish Workshop on Formal Methods

Conference acronym: FM

Conference number: 2

Conference location: Cork, Ireland

Conference date: 2-3 July 1998

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Irish Workshop on Formal Methods

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FM1998.2

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing