Hyperkernel: Push-Button Verification of an OS Kernel.
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.
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.
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. Best paper award
Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang.
In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI), Savannah, GA, November 2016.
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.
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.
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.
Xi Wang, Nickolai Zeldovich, M. Frans Kaashoek, and Armando Solar-Lezama.
Communications of the ACM, 59(3):99–106, March 2016.
Verdi: A Framework for Implementing and Formally Verifying Distributed Systems.
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson.
In Proceedings of the 2015 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.
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.