SAnToS-TR2016-03-11

"Focused Certification of an Industrial Compilation and Static Verification Toolchain".
Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu.
To appear in the proceedings of the 15th International Conference on Software Engineering and Formal Methods (SEFM 2017), Trento, Italy, September 2017.

Supporting Artifacts:

• Experiment Test Programs
• Experiment Results
• Coq Specification, Implementation, and Proofs (with Coq8.5) — Table of Contents [Repository]
  • SPARK Semantics (Specification):
  • AST
  • EVAL (big step operational semantics)
  • SPARK Semantics with Explicit Run-time Check Decorations (Specification):
  • AST-RT
  • EVAL-RT
  • RT-GEN — Certified SPARK Run-time Check Generator:
    • Specification
    • Consistency (Soundness & Completeness) Proof wrt. SPARK Semantics
    • Implementation
    • Consistency Proof wrt. RT-GEN Specification
  • RT-OPT — Certified SPARK Run-time Check Optimizer:
    • Specification
    • Consistency Proof wrt. RT-GEN Specification
    • Implementation
    • Consistency Proof wrt. RT-OPT Specification
  • ⊆ -- Run-time Check Conformance Checker (Implementation, e.g., to compare GNAT against RT-GEN and RT-OPT)
• Bakar Jago: SPARK-to-Coq (AST) Translator