From Event-B to Verified C via HLL

Ning Ge, Arnaud Dieumegard, Eric Jenn +1

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 fina…