eBPF is a machine-language that executes inside the Linux kernel.

PREVAIL is a new verifier that is simple, scalable, and can handle loops of arbitrary number of iterations. The verifier is based on the theory of abstract-interpetation.

• Source code: github.com/vbpf/ebpf-verifier
• Benchmark: github.com/vbpf/ebpf-samples
• You can find more details in the PLDI paper