The Matrix Reproved (Verification Pearl)

Martin Clochard 1, 2 Léon Gondelman 1, 2 Mário Pereira 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops and the Strassen's algorithm. The proofs are conducted using the Why3 platform for deductive program verification, and automated theorem provers to discharge proof obligations. In order to specify and prove the two multiplication algorithms , we develop a new Why3 theory of matrices and apply the proof by reflection methodology.
Type de document :
Communication dans un congrès
VSTTE 2016, Jul 2016, Toronto, Canada
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01316902
Contributeur : Mário José Parreira Pereira <>
Soumis le : mardi 29 novembre 2016 - 13:35:41
Dernière modification le : samedi 18 février 2017 - 01:10:22
Document(s) archivé(s) le : lundi 27 mars 2017 - 08:33:49

Fichier

paper_12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01316902, version 2

Citation

Martin Clochard, Léon Gondelman, Mário Pereira. The Matrix Reproved (Verification Pearl). VSTTE 2016, Jul 2016, Toronto, Canada. 〈hal-01316902v2〉

Partager

Métriques

Consultations de la notice

154

Téléchargements de fichiers

79