Sciweavers

IWFM
1998

Formal Engineering of the Bitonic Sort using PVS

13 years 5 months ago
Formal Engineering of the Bitonic Sort using PVS
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.
Raphaël Couturier
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 1998
Where IWFM
Authors Raphaël Couturier
Comments (0)