The Matrix Reproved : Verification Pearl

Martin Clochard 1 Léon Gondelman 1 Mário Pereira 1
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 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. In order to prove the matrix identities on which Strassen's algorithm is based, we apply the proof by reflection methodology, which we implement using ghost state.To our knowledge, this is the first time such a methodology is used under an auto-active setting.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, pp.1-19. 〈10.1007/s10817-017-9436-2〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01617437
Contributeur : Claude Marché <>
Soumis le : lundi 16 octobre 2017 - 15:32:12
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : mercredi 17 janvier 2018 - 13:51:27

Fichier

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

Identifiants

Citation

Martin Clochard, Léon Gondelman, Mário Pereira. The Matrix Reproved : Verification Pearl. Journal of Automated Reasoning, Springer Verlag, 2017, pp.1-19. 〈10.1007/s10817-017-9436-2〉. 〈hal-01617437〉

Partager

Métriques

Consultations de la notice

162

Téléchargements de fichiers

35