mechanized Semantics

Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA). We develop a small-step …
Cite
Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
Formal Specification of Linux eBPF Instruction Set Architecture in Sail
eBPF has become a widely-used mechanism for extending the Linux kernel, and recent standardization efforts have produced the first …
Cite
Formal Specification of Linux eBPF Instruction Set Architecture in Sail