menu

Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel

Nelson, Luke and Geffen, Jacob Van and Torlak, Emina and Wang, Xi

PDF


@inproceedings{nelson-usenix20,
  author = {Nelson, Luke and Geffen, Jacob Van and Torlak, Emina and Wang, Xi},
  booktitle = {14th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 20)},
  date-added = {2020-11-16 00:10:08 -0800},
  date-modified = {2020-11-16 00:10:15 -0800},
  isbn = {978-1-939133-19-9},
  month = nov,
  pages = {41--61},
  publisher = {{USENIX} Association},
  title = {Specification and verification in the field: Applying formal methods to {BPF} just-in-time compilers in the Linux kernel},
  url = {https://www.usenix.org/conference/osdi20/presentation/nelson},
  year = {2020},
  bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAccGFwZXJzL25lbHNvbi11c2VuaXgyMC1hLnBkZk8RAXwAAAAAAXwAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xVuZWxzb24tdXNlbml4MjAtYS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAEAAwAACiBjdQAAAAAAAAAAAAAAAAAGcGFwZXJzAAIAOy86VXNlcnM6Z2FtYmxpbjI6c3JjOmJ1aWxkLWJpYjpwYXBlcnM6bmVsc29uLXVzZW5peDIwLWEucGRmAAAOACwAFQBuAGUAbABzAG8AbgAtAHUAcwBlAG4AaQB4ADIAMAAtAGEALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADlVc2Vycy9nYW1ibGluMi9zcmMvYnVpbGQtYmliL3BhcGVycy9uZWxzb24tdXNlbml4MjAtYS5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAEMAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABww==},
  bdsk-url-1 = {https://www.usenix.org/conference/osdi20/presentation/nelson}
}

Top