This page is part of an archival collection and is no longer actively maintained.

It may contain outdated information and may not meet current or future WCAG accessibility standards. We provide this content, its subpages, and associated links for historical reference only. If you need assistance, please contact support@cs.washington.edu

UNSAT: Jitterbug

Jitterbug 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

Download

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]