The matrix reproved (verification pearl)

DOI10.1007/s10817-017-9436-2zbMath1426.68164OpenAlexW2763423918MaRDI QIDQ1703015

Peng Zhang

Publication date: 1 March 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01617437/file/main.pdf

zbMATH Keywords

Why3Strassen's algorithmdeductive program verificationproof by reflection

Mathematics Subject Classification ID

Uses Software

• Coq
• Why3
• WhyML
• Jordan Normal Forms
• Archive Formal Proofs

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A Refinement-Based Approach to Computational Algebra in Coq
• One Logic to Use Them All
• From program verification to program synthesis
• Why3 — Where Programs Meet Provers

This page was built for publication: The matrix reproved (verification pearl)