I detta dokument presenteras en metod för att skapa formellt korrekta just-in-time-kompilatorer (JIT). Godtagbarheten av vårt tillvägagångssätt visas genom, vad vi tror är den första, verifiering av en JIT kompilator med avseende på en realistisk semantik av självmodifierande x86 maskinkod. Våra semantik innehåller en modell av instruktionscachen. Två versioner av den verifierade JIT kompilatorn presenteras: en genererar alla maskinkoden på en gång, den andra är inkrementell d.v.s. producerar kod på begäran. Alla bevis har gjorts inne i HOL4 teoremprovaren.
Ett relaterat arbete nyligen i verifieringen av självmodifierande x86-kod baserad på Hoare logik är en av Myreen REF.
Verified just-in-time compiler on x86
{'venue': "POPL '10", 'journal': None, 'mag_field_of_study': ['Computer Science']}