2022

• Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. A Formal Foundation for Symbolic Evaluation with Merging. In Proc. of the 49th ACM Symposium on Principles of Programming Languages (POPL), Jan 2022. [pdf]

2020

• Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In Proc. of the 14th OSDI, Nov 2020. [pdf] [slides]

• Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 54(1), Aug 2020. [pdf]

• Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. Synthesizing JIT Compilers for In-Kernel DSLs. In Proc. of the 32nd International Conference on Computer Aided Verification (CAV), Jul 2020. [pdf]

• Helgi Sigurbjarnarson. Push-Button Verification of Systems Software. PhD thesis, University of Washington, Apr 2020. [pdf]

• Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. Fixing Code That Explodes Under Symbolic Evaluation. In Proc. of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan 2020. [pdf]

2019

• Luke Nelson and Xi Wang. Developing security monitors on RISC-V: Case studies on HiFive Unleashed. Technical Report UW-CSE-2019-11-01, University of Washington, Nov 2019. [pdf]

• Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proc. of the 27th SOSP, Oct 2019. [pdf] [slides] Best paper award Distinguished artifact award

• Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. A note on verifying information flow control systems with Nickel. Technical Report UW-CSE-2019-10-01, University of Washington, Oct 2019. [pdf]

• James Bornholt. Optimizing the Automated Programming Stack. PhD thesis, University of Washington, Aug 2019. [pdf]

2018

• James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. In Proc. of the 33rd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Nov 2018. [pdf] Distinguished artifact award

• Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proc. of the 13th OSDI, Oct 2018. [pdf] [slides]

• Bruno Castro-Karney. A Crash-Safe Key-Value Store Using Chained Copy-on-Write B-trees. Senior Thesis, University of Washington, Jun 2018. [pdf] Best senior thesis award

2017

• Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. In Proc. of the 26th SOSP, Oct 2017. [pdf] [slides]

• Dylan Johnson. Porting Hyperkernel to the ARM Architecture. Technical Report UW-CSE-17-08-02, University of Washington, Aug 2017. [pdf]

• James Bornholt and Emina Torlak. Synthesizing Memory Models from Framework Sketches and Litmus Tests. In Proc. of the 38th PLDI, Jun 2017. [pdf] [slides]

2016

• Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. In Proc. of the 12th OSDI, Nov 2016. [pdf] [slides] Best paper award

• Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. In Proc. of the 28th International Conference on Computer Aided Verification (CAV), Jul 2016. [pdf]

• James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Specifying and Checking File System Crash-Consistency Models. In Proc. of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Apr 2016. [pdf] [slides]

• James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. In Proc. of the 43rd ACM Symposium on Principles of Programming Languages (POPL), Jan 2016. [pdf] [slides]