BPF and formal verification
https://www.sccs.swarthmore.edu/users/16/mmcconv1/pl-reflection.html [www.sccs.swarthmore.edu]
2019-06-07 04:24
I spent the spring of 2015 researching the Berkeley packet filter (BPF) and its formal verification with my programming languages professor, Joe Gibbs Politz. The project took some unexpected turns and we learned a lot about Coq and applied formal verification in the process.
source: HN