mail_outline lukenels location_on Allen Center 591 photo_camera Photo
I am a final-year PhD student in the UNSAT group and systems lab at University of Washington, advised by Xi Wang. Most recently, I have been working on Jitterbug, a framework for writing and verifying BPF JIT compilers in the Linux kernel, and Serval, a framework for building automated verifiers for systems code.
A Formal Foundation for Symbolic Evaluation with Merging.
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak.
In Proceedings of the 49th ACM Symposium on Principles of Programming Languages (POPL), Philadelphia, PA, January 2022.
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. [pdf]
Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang.
In Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Virtual conference, November 2020.
Noninterference specifications for secure systems. [pdf]
Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang.
ACM SIGOPS Operating Systems Review, 54(1), August 2020.
Synthesizing JIT Compilers for In-Kernel DSLs. [pdf]
Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak.
In Proceedings of the 32nd International Conference on Computer Aided Verification (CAV), Los Angeles, CA, July 2020.
Scaling symbolic evaluation for automated verification of systems code with Serval. [pdf] Best paper award Distinguished artifact award
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang.
In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), Huntsville, Ontario, Canada, October 2019.
Nickel: A Framework for Design and Verification of Information Flow Control Systems. [pdf]
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang.
In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Carlsbad, CA, October 2018.
Hyperkernel: Push-Button Verification of an OS Kernel. [pdf]
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang.
In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), Shanghai, China, October 2017.
