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

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
Compiler Synthesis

Links

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

Last commit date

1 May 2020

Related papers

https://doi.org/10.1007/978-3-030-53291-8_29

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.