David Monniaux, Cyril Six. Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. In Jörg Henkel, Xu Liu 0001, editors, LCTES '21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021. pages 85-96, ACM, 2021. [doi]
Abstract is missing.