The Matrix Reproved (Verification Pearl)

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2018-03, Vol.60 (3), p.365-383
Main Authors: Clochard, Martin, Gondelman, Léon, Pereira, Mário
Format: Article
Language:English
Subjects:
Algorithms
Artificial Intelligence
Computer Science
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Multiplication
Nested loops
Program verification (computers)
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-017-9436-2