PV2 JitSynthsynthesises a verified just-in-time compiler for in-kernel domain-specific languages

Application domain/field

Type of tool

Synthesis tool

Expected input

Syntax, semantics and a mapping from source to target states


As a program in a solver-aided host language, e.g. Rosette.

Expected output

A verified JIT compiler that can transform a program in the source DSL into a semantically equivalent program in the target language.


Tool for synthesizing verified JIT (just-in-time) compilers for in-kernel DSLs (domain specific languages). Uses Rosette
Compiler Synthesis


Repository: https://github.com/uw-unsat/jitsynth

Related papers

Synthesizing JIT Compilers for In-Kernel DSLs

Last publication date

14 July 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.