SPARK Formal

The SPARK Formal project aims to develop a complete set of semantics of the SPARK language in Coq, for:

    - at the language level, ensuring the absence of ambiguity and the completeness of evaluation rules
    - at the tool level, ensuring the correct insertion of checks in the AST used for compilation and analysis

The formalization of SPARK also paves the way for the creation of proved toolchains for SPARK programs (a.k.a. “certified” toolchains in academia) such as CompCert.

This entry was posted in Open-DO News. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*
 
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org