Verified just-in-time compiler on x86

This paper presents a method for creating formally correct just-intime (JIT) compilers. The tractability of our approach is demonstrated through, what we believe is the first, verification of a JIT compiler with respect to a realistic semantics of self-modifying x86 machine code. Our semantics includes a model of the instruction cache. Two versions of the verified JIT compiler are presented: one generates all of the machine code at once, the other one is incremental i.e. produces code on-demand. All proofs have been performed inside the HOL4 theorem prover. General Terms software verification, formal methods Keywords self-modifying code, compiler verification, just in time

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Magnus O. Myreen
• Keywords: JIT Compiler, Keywords Self-modifying Code, POPL 2010, Programming Languages, Self-modifying X86 Machine