The Matrix Reproved (Verification Pearl)

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-01316902
Contributor : Mário José Parreira Pereira <>
Submitted on : Tuesday, November 29, 2016 - 1:35:41 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Monday, March 27, 2017 - 8:33:49 AM

File

paper_12.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

254

Files downloads

355