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

Application domain/field

• Domain specific languages (DSLs)
• Program synthesis
• Just-in-time (JIT) compilation

Type of tool

Synthesis tool

Expected input

Syntax, semantics and a mapping from source to target states

Format:

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.

Internals

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