most citedFormally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler

26 citations · 26 across the 1 of their papers we have counts for

collaborators

1 paper

cs.PL2022★ 26 cited

Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler

Aurèle Barrière, Sandrine Blazy, David Pichardie

Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution,…