Hyperkernel: Push-Button Verification of an OS Kernel. - Luke Nelson; Helgi Sigurbjarnarson; Kaiyuan Zhang 001; Dylan Johnson; James Bornholt; Emina Torlak; Xi Wang 005 (SOSP, 2017)

A recursion on maximal chains in the Tamari lattices. - Luke Nelson (Discret. Math., 2017)

Nickel: A Framework for Design and Verification of Information Flow Control Systems. - Helgi Sigurbjarnarson; Luke Nelson; Bruno Castro-Karney; James Bornholt; Emina Torlak; Xi Wang 005 (OSDI, 2018)

Scaling symbolic evaluation for automated verification of systems code with Serval. - Luke Nelson; James Bornholt; Ronghui Gu; Andrew Baumann; Emina Torlak; Xi Wang 005 (SOSP, 2019)

Synthesizing JIT Compilers for In-Kernel DSLs. - Jacob Van Geffen; Luke Nelson; Isil Dillig; Xi Wang 005; Emina Torlak (CAV (2), 2020)

Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. - Luke Nelson; Jacob Van Geffen; Emina Torlak; Xi Wang 005 (OSDI, 2020)

Noninterference specifications for secure systems. - Luke Nelson; James Bornholt; Arvind Krishnamurthy; Emina Torlak; Xi Wang 005 (ACM SIGOPS Oper. Syst. Rev., 2020)

The Tamari block lattice: An order on saturated chains in the Tamari lattice. - Luke Nelson; Kevin Treat (Discret. Math., 2022)

A formal foundation for symbolic evaluation with merging. - Sorawee Porncharoenwase; Luke Nelson; Xi Wang 005; Emina Torlak (Proc. ACM Program. Lang., 2022)

Recursive constructions for the higher Stasheff - Tamari orders in dimension three using the Outer Tamari and Tamari Block posets. - Luke Nelson; Kevin Treat (Discret. Math., 2024)