Journal of Automated Reasoning

, Volume 60, Issue 3, pp 365–383 | Cite as

The Matrix Reproved (Verification Pearl)

Article
  • 66 Downloads

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.

Keywords

Why3 Deductive program verification Strassen’s algorithm Proof by reflection 

Notes

Acknowledgements

This work is partly supported by the Bware (ANR-12-INSE-0010, http://bware.lri.fr/), VOCAL (ANR-15-CE25-008, https://vocal.lri.fr/) Projects of the French National Research Organization (ANR), and by the Portuguese Foundation for the Sciences and Technology (Grant FCT-SFRH/BD/99432/2014). We thank Arthur Charguéraud, Jean-Christophe Filliâtre, and Claude Marché for their comments and remarks.

References

  1. 1.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Berlin (2004)CrossRefMATHGoogle Scholar
  2. 2.
    Boutin, S.: Réflexions sur les quotients. Thèse d’université, Paris 7 (1997)Google Scholar
  3. 3.
    Clochard, M.: Preuves taillées en biseau. In: Vingt-huitièmes Journées Francophones des Langages Applicatifs. Gourette, France (2017)Google Scholar
  4. 4.
    Clochard, M., Filliâtre, J.C., Marché, C., Paskevich, A.: Formalizing semantics with an automatic program verifier. In: Giannakopoulou, D., Kroening, D. (eds.) 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE). Lecture Notes in Computer Science, vol. 8471, pp. 37–51. Springer, Vienna (2014)Google Scholar
  5. 5.
    Dénès, M., Mörtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP: 3rd International Conference on Interactive Theorem Proving-2012. Lecture Notes in Computer Science, vol. 7406, pp. 83–98. Springer, Princeton. http://hal.inria.fr/hal-00734505 (2012)
  6. 6.
    Filliâtre, J.C.: One logic to use them all. In: 24th International Conference on Automated Deduction (CADE-24). Lecture Notes in Artificial Intelligence, vol. 7898, pp. 1–20. Springer, Lake Placid (2013)Google Scholar
  7. 7.
    Filliâtre, J.C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Biere, A., Bloem, R. (eds.) 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 8859, pp. 1–16. Springer, Vienna (2014)Google Scholar
  8. 8.
    Filliâtre, J.C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Proceedings of the 22nd European Symposium on Programming. Lecture Notes in Computer Science, vol. 7792, pp. 125–128. Springer, Berlin (2013)Google Scholar
  9. 9.
    Palomo-Lozano, F., Medina-Bulo, I., Alonso-Jiménez, J.: Certification of matrix multiplication algorithms. Strassen’s algorithm in ACL2. In: Supplemental Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pp. 283–298, Edinburgh, Scotland (2001)Google Scholar
  10. 10.
    Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 313–326. POPL ’10, ACM, New York. (2010). doi: 10.1145/1706299.1706337
  11. 11.
    The Coq Development Team: The Coq Proof Assistant Reference Manual—Version V8.6. http://coq.inria.fr (2016)
  12. 12.
    Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs 2015. https://www.isa-afp.org/entries/Jordan_Normal_Form.shtml (2015)

Copyright information

© Springer Science+Business Media B.V. 2017

Authors and Affiliations

  1. 1.Lab. de Recherche en Informatique, CNRSUniv. Paris-SudOrsayFrance
  2. 2.INRIAUniversité Paris-SaclayPalaiseauFrance

Personalised recommendations