From Event-B to Verified C via HLL

Preprint English OPEN
Ge , Ning; Dieumegard , Arnaud; Jenn , Eric; Voisin , Laurent;
  • Publisher: HAL CCSD
  • Subject: S3 | C | Property proof | HLL | Computer Science - Software Engineering | Equivalence proof | [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF] | [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] | Code generation | [ INFO.INFO-SE ] Computer Science [cs]/Software Engineering [cs.SE] | [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] | [ INFO.INFO-PF ] Computer Science [cs]/Performance [cs.PF] | Event-B | [ INFO.INFO-SC ] Computer Science [cs]/Symbolic Computation [cs.SC]

This work addresses the correct translation of an Event-B model to C code via an intermediate formal language, HLL. The proof of correctness follows two main steps. First, the final refinement of the Event-B model, including in-variants, is translated to HLL. At that po... View more
Share - Bookmark