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), Banff, Alberta, Canada, 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.
Automated Verification of Customizable Middlebox Properties with Gravel. [pdf]
Kaiyuan Zhang, Danyang Zhuo, Aditya Akella, Arvind Krishnamurthy, and Xi Wang.
In Proceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI), Santa Clara, CA, February 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.
MultiNyx: A Multi-Level Abstraction Framework for Systematic Analysis of Hypervisors. [pdf]
Pedro Fonseca, Xi Wang, and Arvind Krishnamurthy.
In Proceedings of the 13th ACM EuroSys Conference, Porto, Portugal, April 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.
Customizing Progressive JPEG for Efficient Image Storage. [pdf]
Eddie Yan, Kaiyuan Zhang, Xi Wang, Karin Strauss, and Luis Ceze.
In Proceedings of the 9th USENIX Workshop on Hot Topics in Storage and File Systems (HotStorage), Santa Clara, CA, July 2017.
An Empirical Study on the Correctness of Formally Verified Distributed Systems. [pdf]
Pedro Fonseca, Kaiyuan Zhang, Xi Wang, and Arvind Krishnamurthy.
In Proceedings of the 12th ACM EuroSys Conference, Belgrade, Serbia, April 2017.
Push-Button Verification of File Systems via Crash Refinement. [pdf] Best paper award
Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang.
In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Savannah, GA, November 2016.
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. [pdf]
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky.
In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), Toronto, Canada, July 2016.
Specifying and Checking File System Crash-Consistency Models. [pdf]
James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang.
In Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Atlanta, GA, April 2016.
A Differential Approach to Undefined Behavior Detection. [pdf]
Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama.
Communications of the ACM, 59(3), March 2016.
Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. [pdf]
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson.
In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Portland, OR, June 2015.
Toward a Dependability Case Language and Workflow for a Radiation Therapy System. [pdf]
Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang.
In Proceedings of the 1st Summit on Advances in Programming Languages (SNAPL), Asilomar, CA, May 2015.
A Differential Approach to Undefined Behavior Detection. [pdf]
Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama.
ACM Transactions on Computer Systems, 33(1), March 2015.
Cybertron: Pushing the Limit on I/O Reduction in Data-Parallel Programs. [pdf]
Tian Xiao, Zhenyu Guo, Hucheng Zhou, Jiaxing Zhang, Xu Zhao, Chencheng Ye, Xi Wang, Wei Lin, Wenguang Chen, and Lidong Zhou.
In Proceedings of the 2014 Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Portland, OR, October 2014.
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. [pdf]
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock.
In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Broomfield, CO, October 2014.
Identifying information disclosure in web applications with retroactive auditing. [pdf]
Haogang Chen, Taesoo Kim, Xi Wang, M. Frans Kaashoek, and Nickolai Zeldovich.
In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Broomfield, CO, October 2014.
Why does cryptographic software fail? A case study and open problems. [pdf]
David Lazar, Haogang Chen, Xi Wang, and Nickolai Zeldovich.
In Proceedings of the 5th Asia-Pacific Workshop on Systems, Beijing, China, June 2014.
Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior. [pdf] Best paper award
Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama.
In Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP), Farmington, PA, November 2013.
Security bugs in embedded interpreters. [pdf]
Haogang Chen, Cody Cutler, Taesoo Kim, Yandong Mao, Xi Wang, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 4th Asia-Pacific Workshop on Systems, Singapore, July 2013.
Improving Integer Security for Systems with Kint. [pdf]
Xi Wang, Haogang Chen, Zhihao Jia, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Hollywood, CA, October 2012.
Undefined Behavior: What Happened to My Code? [pdf]
Xi Wang, Haogang Chen, Alvin Cheung, Zhihao Jia, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 3rd Asia-Pacific Workshop on Systems, Seoul, South Korea, July 2012.
Software fault isolation with API integrity and multi-principal modules. [pdf]
Yandong Mao, Haogang Chen, Dong Zhou, Xi Wang, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP), Cascais, Portugal, October 2011.
Retroactive auditing. [pdf]
Xi Wang, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 2nd Asia-Pacific Workshop on Systems, Shanghai, China, July 2011.
Linux kernel vulnerabilities: State-of-the-art defenses and open problems. [pdf]
Haogang Chen, Yandong Mao, Xi Wang, Dong Zhou, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 2nd Asia-Pacific Workshop on Systems, Shanghai, China, July 2011.
Language-Based Replay via Data Flow Cut. [pdf]
Ming Wu, Fan Long, Xi Wang, Zhilei Xu, Haoxiang Lin, Xuezheng Liu, Zhenyu Guo, Huayang Guo, Lidong Zhou, and Zheng Zhang.
In Proceedings of the 18th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), Santa Fe, NM, November 2010.
Intrusion Recovery Using Selective Re-execution. [pdf]
Taesoo Kim, Xi Wang, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Vancouver, Canada, October 2010.
Improving Application Security with Data Flow Assertions. [pdf]
Alexander Yip, Xi Wang, Nickolai Zeldovich, and M. Frans Kaashoek.
In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), Big Sky, MT, October 2009.
API Hyperlinking via Structural Overlap. [pdf]
Fan Long, Xi Wang, and Yang Cai.
In Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Amsterdam, The Netherlands, August 2009.
R2: An Application-Level Kernel for Record and Replay. [pdf]
Zhenyu Guo, Xi Wang, Jian Tang, Xuezheng Liu, Zhilei Xu, Ming Wu, M. Frans Kaashoek, and Zheng Zhang.
In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), San Diego, CA, December 2008.
Towards Automatic Inference of Task Hierarchies in Complex Systems. [pdf]
Haohui Mai, Chongnan Gao, Xuezheng Liu, Xi Wang, and Geoffrey M. Voelker.
In Proceedings of the 4th Workshop on Hot Topics in System Dependability (HotDep), San Diego, CA, December 2008.
Conditional Correlation Analysis for Safe Region-based Memory Management. [pdf]
Xi Wang, Zhilei Xu, Xuezheng Liu, Zhenyu Guo, Xiaoge Wang, and Zheng Zhang.
In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Tucson, AZ, June 2008.
D3S: Debugging Deployed Distributed Systems. [pdf]
Xuezheng Liu, Zhenyu Guo, Xi Wang, Feibo Chen, Xiaochen Lian, Jian Tang, Ming Wu, M. Frans Kaashoek, and Zheng Zhang.
In Proceedings of the 5th USENIX Symposium on Networked Systems Design and Implementation (NSDI), San Francisco, CA, April 2008.
Hang Analysis: Fighting Responsiveness Bugs. [pdf] Best student paper award
Xi Wang, Zhenyu Guo, Xuezheng Liu, Zhilei Xu, Haoxiang Lin, Xiaoge Wang, and Zheng Zhang.
In Proceedings of the 3rd ACM EuroSys Conference, Glasgow, Scotland, April 2008.