BPF and formal verification
https://www.sccs.swarthmore.edu/users/16/mmcconv1/pl-reflection.html [www.sccs.swarthmore.edu]
2017-01-12 04:29
Intro to BPF (specifically the OpenBSD flavor, though without loss of generality) and verification.
BPF is also a fantastic target for formal verification because it can only jump forward. This avoids the halting problem – BPF programs have a finite set of possible states and must terminate. We can therefore model BPF and analyze its programs completely rather than resorting to heuristics that give false positives.
source: L