| 2026 | ECOOP | A Complete Program Logic for Compositional Linearizability. | Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, Zhong Shao |
| 2026 | Mobisys | Ringmaster: How to juggle high-throughput host OS system calls from TrustZone TEEs. | Richard Thomas Habeeb, Man-Ki Yoon, Hao Chen, Zhong Shao |
| 2026 | SP | Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol Under the LiDO-DAG Framework. | Longfei Qiu, Jingqi Xiao, Zhong Shao |
| 2025 | ACSAC | It's a Non-Stop PARTEE! Practical Multi-Enclave Availability Through Partitioning and Asynchrony. | Richard Habeeb, Hao Chen, Man-Ki Yoon, Zhong Shao |
| 2023 | CCS | Ou: Automating the Parallelization of Zero-Knowledge Protocols. | Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao |
| 2022 | DSN | TimeDice: Schedulability-Preserving Priority Inversion for Mitigating Covert Timing Channels Between Real-time Partitions. | Man-Ki Yoon, Jung-Eun Kim, Richard M. Bradford, Zhong Shao |
| 2022 | PLDI | Adore: atomic distributed objects with certified reconfiguration. | Wolf Honor, Ji-Yong Shin, Jieung Kim, Zhong Shao |
| 2021 | DATE | Adaptive Generative Modeling in Resource-Constrained Environments. | Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao |
| 2021 | DATE | Paired Training Framework for Time-Constrained Learning. | Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao |
| 2021 | PLDI | CompCertO: compiling certified open C components. | Jrmie Koenig, Zhong Shao |
| 2020 | DATE | AnytimeNet: Controlling Time-Quality Tradeoffs in Deep Neural Network Architectures. | Jung-Eun Kim, Richard M. Bradford, Zhong Shao |
| 2020 | DATE | ABC: Abstract prediction Before Concreteness. | Jung-Eun Kim, Richard M. Bradford, Man-Ki Yoon, Zhong Shao |
| 2020 | ICRA | Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems. | Valerie Chen, Man-Ki Yoon, Zhong Shao |
| 2020 | LICS | Refinement-Based Game Semantics for Certified Abstraction Layers. | Jrmie Koenig, Zhong Shao |
| 2019 | CAV | Integrating Formal Schedulability Analysis into a Verified OS Kernel. | Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao |
| 2019 | CLOUD | WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. | Ji-Yong Shin, Jieung Kim, Wolf Honor, Hernn Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, Zhong Shao |
| 2019 | DSN | Novelty Detection via Network Saliency in Visual-Based Deep Learning. | Valerie Chen, Man-Ki Yoon, Zhong Shao |
| 2019 | ICDCS | ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems. | Man-Ki Yoon, Zhong Shao |
| 2018 | PLDI | Certified concurrent abstraction layers. | Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jrmie Koenig, Vilhelm Sjberg, Hao Chen, David Costanzo, Tahina Ramananandro |
| 2017 | APLAS | Safety and Liveness of MCS Lock - Layer by Layer. | Jieung Kim, Vilhelm Sjberg, Ronghui Gu, Zhong Shao |
| 2017 | CAV | Automated Resource Analysis with Coq Proof Objects. | Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao |
| 2016 | OSDI | CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. | Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjberg, David Costanzo |
| 2016 | PLDI | Toward compositional verification of interruptible OS kernels and device drivers. | Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu |
| 2016 | PLDI | End-to-end verification of information-flow security for C and assembly programs. | David Costanzo, Zhong Shao, Ronghui Gu |
| 2015 | CPP | A Compositional Semantics for Verified Separate Compilation and Linking. | Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jrmie Koenig, Yuchen Fu |
| 2015 | CPP | Clean-Slate Development of Certified OS Kernels. | Zhong Shao |
| 2015 | ESOP | Automatic Static Cost Analysis for Parallel Programs. | Jan Hoffmann, Zhong Shao |
| 2015 | PLDI | Compositional certified resource bounds. | Quentin Carbonneaux, Jan Hoffmann, Zhong Shao |
| 2015 | POPL | Deep Specifications and Certified Abstraction Layers. | Ronghui Gu, Jrmie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo |
| 2014 | CSL | Compositional verification of termination-preserving refinement of concurrent programs. | Hongjin Liang, Xinyu Feng, Zhong Shao |
| 2014 | FLOPS | Type-Based Amortized Resource Analysis with Integers and Arrays. | Jan Hoffmann, Zhong Shao |
| 2014 | PLDI | End-to-end verification of stack-space bounds for C programs. | Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao |
| 2014 | TASE | Trace-Based Temporal Verification for Message-Passing Programs. | Jinjiang Lei, Zongyan Qiu, Zhong Shao |
| 2013 | CONCUR | Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. | Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao |
| 2013 | LICS | Quantitative Reasoning for Proving Lock-Freedom. | Jan Hoffmann, Michael Marmar, Zhong Shao |
| 2012 | APLAS | A Case for Behavior-Preserving Actions in Separation Logic. | David Costanzo, Zhong Shao |
| 2012 | APLAS | Modular Verification of Concurrent Thread Management. | Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi |
| 2012 | CPP | Compositional Verification of a Baby Virtual Memory Manager. | Alexander Vaynberg, Zhong Shao |
| 2012 | ICRA | Proving the correctness of concurrent robot software. | Peter Kazanzides, Yanni Kouskoulas, Anton Deguet, Zhong Shao |
| 2012 | POPL | Static and user-extensible proof checking. | Antonis Stampoulis, Zhong Shao |
| 2012 | TAMC | A Structural Approach to Prophecy Variables. | Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, Yong Li |
| 2011 | TASE | A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. | Wei Wang, Zhong Shao, Xinyu Jiang, Yu Guo |
| 2010 | CONCUR | Reasoning about Optimistic Concurrency Using a Program Logic for History. | Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang |
| 2010 | ESOP | Parameterized Memory Models and Concurrent Separation Logic. | Rodrigo Ferreira, Xinyu Feng, Zhong Shao |
| 2010 | ICFP | VeriML: typed computation of logical terms inside a language with effects. | Antonis Stampoulis, Zhong Shao |
| 2009 | APLAS | Weak updates and separation logic. | Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai |
| 2009 | TASE | Modular Development of Certified System Software. | Zhong Shao |
| 2008 | PLDI | Certifying low-level programs with hardware interrupts and preemptive threads. | Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo |
| 2007 | ESOP | On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. | Xinyu Feng, Rodrigo Ferreira, Zhong Shao |
| 2007 | PLDI | Certified self-modifying code. | Hongxu Cai, Zhong Shao, Alexander Vaynberg |
| 2007 | PLDI | A general framework for certifying garbage collectors and their mutators. | Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li |
| 2007 | TASE | Foundational Typed Assembly Language with Certified Garbage Collection. | Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo |
| 2006 | PLDI | Modular verification of assembly code with stack-based control abstractions. | Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni |
| 2006 | POPL | Certified assembly programming with embedded code pointers. | Zhaozhong Ni, Zhong Shao |
| 2005 | ICFP | Modular verification of concurrent assembly code with dynamic thread creation and termination. | Xinyu Feng, Zhong Shao |
| 2004 | ICFP | Verification of safety properties for concurrent assembly code. | Dachuan Yu, Zhong Shao |
| 2003 | CC | Precision in Practice: A Type-Preserving Java Compiler. | Christopher League, Zhong Shao, Valery Trifonov |
| 2003 | ESOP | Building Certified Libraries for PCC: Dynamic Storage Allocation. | Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao |
| 2002 | LICS | A Syntactic Approach to Foundational Proof-Carrying Code. | Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni |
| 2002 | POPL | A type system for certified binaries. | Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou |
| 2001 | PLDI | Principled Scavenging. | Stefan Monnier, Bratin Saha, Zhong Shao |
| 2000 | ICFP | Fully reflexive intensional type analysis. | Valery Trifonov, Bratin Saha, Zhong Shao |
| 1999 | ESOP | Safe and Principled Language Interoperation. | Valery Trifonov, Zhong Shao |
| 1999 | ICFP | Representing Java Classes in a Typed Intermediate Language. | Christopher League, Zhong Shao, Valery Trifonov |
| 1999 | ICFP | Transparent Modules with Fully Syntactic Signatures. | Zhong Shao |
| 1998 | ICFP | Typed Cross-Module Compilation. | Zhong Shao |
| 1998 | ICFP | Implementing Typed Intermediate Languages. | Zhong Shao, Christopher League, Stefan Monnier |
| 1997 | ICFP | Flexible Representation Analysis. | Zhong Shao |
| 1995 | PLDI | A Type-Based Compiler for Standard ML. | Zhong Shao, Andrew W. Appel |
| 1993 | POPL | Smartest Recompilation. | Zhong Shao, Andrew W. Appel |