Jitterbug

Jitterbug is a framework for writing just-in-time (JIT) compilers and proving them correct. It provides a precise specification of JIT correctness and an automated verification strategy that scales to practical implementations.

Jitterbug builds on Serval and Rosette.

Applications

• BPF JITs in the Linux kernel

Download

• Jitterbug development repository

Publications

• Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In Proc. of the 14th OSDI, Nov 2020. [pdf] [slides]