506 citations · 656 across the 2 of their papers we have counts for
2 papers
cs.LO2009★ 506 cited
A formally verified compiler back-end
Xavier Leroy
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to Po…
cs.PL2009★ 150 cited
Mechanized semantics for the Clight subset of the C language
Sandrine Blazy, Xavier Leroy
This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, "struct" and "union" types, C loops and structured…