Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion

David Monniaux, Cyril Six

Appearing at LCTES: Languages, Compilers, Tools and Theory of Embedded Systems