Blog
About

137
views
0
recommends
+1 Recommend
1 collections
    4
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Formal engineering of the bitonic sort using PVS

      2nd Irish Workshop on Formal Methods (FM)

      Irish Workshop on Formal Methods

      2-3 July 1998

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references 2

          • Record: found
          • Abstract: not found
          • Article: not found

          The temporal logic of actions

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Powerlist: a structure for parallel recursion

             Jayadev Misra (1994)
              Bookmark

              Author and article information

              Contributors
              Conference
              July 1998
              July 1998
              : 1-19
              Affiliations
              LORIA - UMR n°7503 - CNRS, Université Henri Poincaré

              BP 239, 54506 Vandœuvre-lés-Nancy, France
              Article
              10.14236/ewic/FM1998.2
              © Raphaël Couturier. Published by BCS Learning and Development Ltd. 2nd Irish Workshop on Formal Methods, Cork, Ireland

              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/

              2nd Irish Workshop on Formal Methods
              FM
              2
              Cork, Ireland
              2-3 July 1998
              Electronic Workshops in Computing (eWiC)
              Irish Workshop on Formal Methods
              Product
              Product Information: 1477-9358BCS Learning & Development
              Self URI (journal page): https://ewic.bcs.org/
              Categories
              Electronic Workshops in Computing

              Comments

              Comment on this article