[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Appel, A.W.: Compiling with Continuations. Cambridge University Press (1992)

  2. Balaa, A., Bertot, Y.: Fonctions récursives générales par itération en théorie des types. In: Journées Francophones des Langages Applicatifs 2002, pp. 27–42. INRIA (2002)

  3. Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS’06). Lecture Notes in Computer Science, vol. 3945, pp. 114–129. Springer (2006)

  4. Bertot, Y., Castéran, P.: Interactive theorem proving and program development—Coq’Art: the calculus of inductive constructions. EATCS Texts in Theoretical Computer Science. Springer (2004)

  5. Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol. 3839, pp. 66–81. Springer (2006)

  6. Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 460–475. Springer (2006)

  7. Coq Development Team: the Coq proof assistant. Software and documentation available at http://coq.inria.fr/ (1989–2007)

  8. Filliâtre, J.C.: Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13(4), 709–745 (2003)

    Article  MATH  Google Scholar 

  9. Filliâtre, J.C.: The Why software verification tool. Software and documentation available at http://why.lri.fr/ (2003–2007)

  10. Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42–54. ACM Press (2006)

  11. Leroy, X., Doligez, D., Garrigue, J., Vouillon, J.: The Objective Caml system. Software and documentation available at http://caml.inria.fr/ (1996–2007)

  12. Letouzey, P.: A new extraction for Coq. In: Types for Proofs and Programs, Workshop TYPES 2002. Lecture Notes in Computer Science, vol. 2646, pp. 200–219. Springer (2003)

  13. May, C.: The parallel assignment problem redefined. IEEE Trans. Softw. Eng. 15(6), 821–824 (1989)

    Article  Google Scholar 

  14. Sethi, R.: A note on implementing parallel assignment instructions. Inf. Process. Lett. 2(4), 91–95 (1973)

    Article  MATH  Google Scholar 

  15. Welch, P.H.: Parallel assignment revisited. Software Practice and Experience 13(12), 1175–1180 (1983)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia—Antipolis Méditerranée, B.P. 93, 06902, Sophia-Antipolis, France

    Laurence Rideau & Bernard Paul Serpette

  2. INRIA Paris—Rocquencourt, B.P. 105, 78153, Le Chesnay, France

    Xavier Leroy

Authors
  1. Laurence Rideau
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernard Paul Serpette
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xavier Leroy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xavier Leroy.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Rideau, L., Serpette, B.P. & Leroy, X. Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves. J Autom Reasoning 40, 307–326 (2008). https://doi.org/10.1007/s10817-007-9096-8

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-007-9096-8

Keywords

Search

Navigation