Callee-Save Registers in Continuation-Passing Style. - Andrew W. Appel; Zhong Shao 001 (LISP Symb. Comput., 1992)

Smartest Recompilation. - Zhong Shao 001; Andrew W. Appel (POPL, 1993)

Space-Efficient Closure Representations. - Zhong Shao 001; Andrew W. Appel (LISP and Functional Programming, 1994)

Unrolling Lists. - Zhong Shao 001; John H. Reppy; Andrew W. Appel (LISP and Functional Programming, 1994)

A Type-Based Compiler for Standard ML. - Zhong Shao 001; Andrew W. Appel (PLDI, 1995)

Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures. - Andrew W. Appel; Zhong Shao 001 (J. Funct. Program., 1996)

Flexible Representation Analysis. - Zhong Shao 001 (ICFP, 1997)

Typed Cross-Module Compilation. - Zhong Shao 001 (ICFP, 1998)

Implementing Typed Intermediate Languages. - Zhong Shao 001; Christopher League; Stefan Monnier (ICFP, 1998)

Optimal Type Lifting. - Bratin Saha; Zhong Shao 001 (Types in Compilation, 1998)

Type-Directed Continuation Allocation. - Zhong Shao 001; Valery Trifonov (Types in Compilation, 1998)

Safe and Principled Language Interoperation. - Valery Trifonov; Zhong Shao 001 (ESOP, 1999)

Representing Java Classes in a Typed Intermediate Language. - Christopher League; Zhong Shao 001; Valery Trifonov (ICFP, 1999)

Transparent Modules with Fully Syntactic Signatures. - Zhong Shao 001 (ICFP, 1999)

Fully reflexive intensional type analysis. - Valery Trifonov; Bratin Saha; Zhong Shao 001 (ICFP, 2000)

Typed common intermediate format. - Zhong Shao 001 (ACM SIGSOFT Softw. Eng. Notes, 2000)

Efficient and safe-for-space closure conversion. - Zhong Shao 001; Andrew W. Appel (ACM Trans. Program. Lang. Syst., 2000)

Principled Scavenging. - Stefan Monnier; Bratin Saha; Zhong Shao 001 (PLDI, 2001)

Invited Talk: Towards a Principled Multi-Language Infrastructure. - Zhong Shao 001 (BABEL, 2001)

Supporting Binary Compatibility with Static Compilation. - Dachuan Yu; Zhong Shao 001; Valery Trifonov (Java Virtual Machine Research and Technology Symposium, 2002)

Type-preserving compilation of Featherweight Java. - Christopher League; Zhong Shao 001; Valery Trifonov (ACM Trans. Program. Lang. Syst., 2002)

Precision in Practice: A Type-Preserving Java Compiler. - Christopher League; Zhong Shao 001; Valery Trifonov (CC, 2003)

A Syntactic Approach to Foundational Proof-Carrying Code. - Nadeem Abdul Hamid; Zhong Shao 001; Valery Trifonov; Stefan Monnier; Zhaozhong Ni (J. Autom. Reason., 2003)

Inlining as staged computation. - Stefan Monnier; Zhong Shao 001 (J. Funct. Program., 2003)

Intensional analysis of quantified types. - Bratin Saha; Valery Trifonov; Zhong Shao 001 (ACM Trans. Program. Lang. Syst., 2003)

Verification of safety properties for concurrent assembly code. - Dachuan Yu; Zhong Shao 001 (ICFP, 2004)

Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. - Nadeem Abdul Hamid; Zhong Shao 001 (TPHOLs, 2004)

Building certified libraries for PCC: dynamic storage allocation. - Dachuan Yu; Nadeem Abdul Hamid; Zhong Shao 001 (Sci. Comput. Program., 2004)

Modular verification of concurrent assembly code with dynamic thread creation and termination. - Xinyu Feng 001; Zhong Shao 001 (ICFP, 2005)

A type system for certified binaries. - Zhong Shao 001; Valery Trifonov; Bratin Saha; Nikolaos Papaspyrou (ACM Trans. Program. Lang. Syst., 2005)

Modular verification of assembly code with stack-based control abstractions. - Xinyu Feng 001; Zhong Shao 001; Alexander Vaynberg; Sen Xiang; Zhaozhong Ni (PLDI, 2006)

Certified assembly programming with embedded code pointers. - Zhaozhong Ni; Zhong Shao 001 (POPL, 2006)

On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. - Xinyu Feng 001; Rodrigo Ferreira; Zhong Shao 001 (ESOP, 2007)

Certified self-modifying code. - Hongxu Cai; Zhong Shao 001; Alexander Vaynberg (PLDI, 2007)

A general framework for certifying garbage collectors and their mutators. - Andrew McCreight; Zhong Shao 001; Chunxiao Lin; Long Li (PLDI, 2007)

Foundational Typed Assembly Language with Certified Garbage Collection. - Chunxiao Lin; Andrew McCreight; Zhong Shao 001; Yiyun Chen; Yu Guo (TASE, 2007)

An open framework for foundational proof-carrying code. - Xinyu Feng 001; Zhaozhong Ni; Zhong Shao 001; Yu Guo (TLDI, 2007)

Using XCAP to Certify Realistic Systems Code: Machine Context Management. - Zhaozhong Ni; Dachuan Yu; Zhong Shao 001 (TPHOLs, 2007)

Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. - Xinyu Feng 001; Zhong Shao 001; Yu Guo; Yuan Dong (VSTTE, 2008)

Modular Development of Certified System Software. - Zhong Shao 001 (TASE, 2009)

Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. - Xinyu Feng 001; Zhong Shao 001; Yu Guo; Yuan Dong (J. Autom. Reason., 2009)

Reasoning about Optimistic Concurrency Using a Program Logic for History. - Ming Fu; Yong Li; Xinyu Feng 001; Zhong Shao 001; Yu Zhang 086 (CONCUR, 2010)

Parameterized Memory Models and Concurrent Separation Logic. - Rodrigo Ferreira; Xinyu Feng 001; Zhong Shao 001 (ESOP, 2010)

VeriML: typed computation of logical terms inside a language with effects. - Antonis Stampoulis; Zhong Shao 001 (ICFP, 2010)

Certified software. - Zhong Shao 001 (Commun. ACM, 2010)

CertiKOS: a certified kernel for secure cloud computing. - Liang Gu; Alexander Vaynberg; Bryan Ford; Zhong Shao 001; David Costanzo (APSys, 2011)

A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. - Wei Wang; Zhong Shao 001; Xinyu Jiang; Yu Guo (TASE, 2011)

Weak Updates and Separation Logic. - Gang Tan; Zhong Shao 001; Xinyu Feng 001; Hongxu Cai (New Gener. Comput., 2011)

A Case for Behavior-Preserving Actions in Separation Logic. - David Costanzo; Zhong Shao 001 (APLAS, 2012)

Modular Verification of Concurrent Thread Management. - Yu Guo; Xinyu Feng 001; Zhong Shao 001; Peizhi Shi (APLAS, 2012)

Compositional Verification of a Baby Virtual Memory Manager. - Alexander Vaynberg; Zhong Shao 001 (CPP, 2012)

Proving the correctness of concurrent robot software. - Peter Kazanzides; Yanni Kouskoulas; Anton Deguet; Zhong Shao 001 (ICRA, 2012)

Static and user-extensible proof checking. - Antonis Stampoulis; Zhong Shao 001 (POPL, 2012)

A Structural Approach to Prophecy Variables. - Zipeng Zhang; Xinyu Feng 001; Ming Fu; Zhong Shao 001; Yong Li (TAMC, 2012)

Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. - Hongjin Liang 001; Jan Hoffmann 002; Xinyu Feng 001; Zhong Shao 001 (CONCUR, 2013)

Quantitative Reasoning for Proving Lock-Freedom. - Jan Hoffmann 002; Michael Marmar; Zhong Shao 001 (LICS, 2013)

Compositional verification of termination-preserving refinement of concurrent programs. - Hongjin Liang 001; Xinyu Feng 001; Zhong Shao 001 (CSL-LICS, 2014)

End-to-end verification of stack-space bounds for C programs. - Quentin Carbonneaux; Jan Hoffmann 002; Tahina Ramananandro; Zhong Shao 001 (PLDI, 2014)

A Separation Logic for Enforcing Declarative Information Flow Control Policies. - David Costanzo; Zhong Shao 001 (POST, 2014)

Trace-Based Temporal Verification for Message-Passing Programs. - Jinjiang Lei; Zongyan Qiu; Zhong Shao 001 (TASE, 2014)

A Compositional Semantics for Verified Separate Compilation and Linking. - Tahina Ramananandro; Zhong Shao 001; Shu-Chun Weng; Jérémie Koenig; Yuchen Fu (CPP, 2015)

Clean-Slate Development of Certified OS Kernels. - Zhong Shao 001 (CPP, 2015)

Automatic Static Cost Analysis for Parallel Programs. - Jan Hoffmann 002; Zhong Shao 001 (ESOP, 2015)

Compositional certified resource bounds. - Quentin Carbonneaux; Jan Hoffmann 002; Zhong Shao 001 (PLDI, 2015)

Deep Specifications and Certified Abstraction Layers. - Ronghui Gu; Jérémie Koenig; Tahina Ramananandro; Zhong Shao 001; Xiongnan (Newman) Wu; Shu-Chun Weng; Haozhong Zhang; Yu Guo (POPL, 2015)

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). - Lars Birkedal; Derek Dreyer; Philippa Gardner; Zhong Shao 001 (Dagstuhl Reports, 2015)

Type-based amortized resource analysis with integers and arrays. - Jan Hoffmann 002; Zhong Shao 001 (J. Funct. Program., 2015)

CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Xiongnan (Newman) Wu; Jieung Kim; Vilhelm Sjöberg; David Costanzo (OSDI, 2016)

End-to-end verification of information-flow security for C and assembly programs. - David Costanzo; Zhong Shao 001; Ronghui Gu (PLDI, 2016)

Safety and Liveness of MCS Lock - Layer by Layer. - Jieung Kim; Vilhelm Sjöberg; Ronghui Gu; Zhong Shao 001 (APLAS, 2017)

Automated Resource Analysis with Coq Proof Objects. - Quentin Carbonneaux; Jan Hoffmann 002; Thomas W. Reps; Zhong Shao 001 (CAV (2), 2017)

Certified concurrent abstraction layers. - Ronghui Gu; Zhong Shao 001; Jieung Kim; Xiongnan (Newman) Wu; Jérémie Koenig; Vilhelm Sjöberg; Hao Chen 023; David Costanzo; Tahina Ramananandro (PLDI, 2018)

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. - Hao Chen 023; Xiongnan (Newman) Wu; Zhong Shao 001; Joshua Lockerman; Ronghui Gu (J. Autom. Reason., 2018)

Integrating Formal Schedulability Analysis into a Verified OS Kernel. - Xiaojie Guo 003; Maxime Lesourd; Mengqi Liu 001; Lionel Rieg; Zhong Shao 001 (CAV (2), 2019)

WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. - Ji-Yong Shin; Jieung Kim; Wolf Honoré; Hernán Vanzetto; Srihari Radhakrishnan; Mahesh Balakrishnan 001; Zhong Shao 001 (SoCC, 2019)

Novelty Detection via Network Saliency in Visual-Based Deep Learning. - Valerie Chen; Man-Ki Yoon; Zhong Shao 001 (DSN Workshops, 2019)

ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems. - Man-Ki Yoon; Zhong Shao 001 (ICDCS, 2019)

Building certified concurrent OS kernels. - Ronghui Gu; Zhong Shao 001; Hao Chen 023; Jieung Kim; Jérémie Koenig; Xiongnan (Newman) Wu; Vilhelm Sjöberg; David Costanzo (Commun. ACM, 2019)

TaskShuffler++: Real-Time Schedule Randomization for Reducing Worst-Case Vulnerability to Timing Inference Attacks. - Man-Ki Yoon; Jung-Eun Kim; Richard M. Bradford; Zhong Shao 001 (CoRR, 2019)

A new hierarchical software architecture towards safety-critical aspects of a drone system. - Xiaorui Zhu; Chen Liang; Zhen-guo Yin; Zhong Shao 001; Meng-qi Liu 001; Hao Chen 023 (Frontiers Inf. Technol. Electron. Eng., 2019)

DeepSEA: a language for certified system software. - Vilhelm Sjöberg; Yuyang Sang; Shu-Chun Weng; Zhong Shao 001 (Proc. ACM Program. Lang., 2019)

An abstract stack based approach to verified compositional compilation to machine code. - Yuting Wang 001; Pierre Wilke; Zhong Shao 001 (Proc. ACM Program. Lang., 2019)

AnytimeNet: Controlling Time-Quality Tradeoffs in Deep Neural Network Architectures. - Jung-Eun Kim; Richard M. Bradford; Zhong Shao 001 (DATE, 2020)

ABC: Abstract prediction Before Concreteness. - Jung-Eun Kim; Richard M. Bradford; Man-Ki Yoon; Zhong Shao 001 (DATE, 2020)

Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems. - Valerie Chen; Man-Ki Yoon; Zhong Shao 001 (ICRA, 2020)

Refinement-Based Game Semantics for Certified Abstraction Layers. - Jérémie Koenig; Zhong Shao 001 (LICS, 2020)

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. - Mengqi Liu 001; Lionel Rieg; Zhong Shao 001; Ronghui Gu; David Costanzo; Jung-Eun Kim; Man-Ki Yoon (Proc. ACM Program. Lang., 2020)

CompCertELF: verified separate compilation of C programs into ELF object files. - Yuting Wang 001; Xiangzhe Xu; Pierre Wilke; Zhong Shao 001 (Proc. ACM Program. Lang., 2020)

Adaptive Generative Modeling in Resource-Constrained Environments. - Jung-Eun Kim; Richard M. Bradford; Max Del Giudice; Zhong Shao 001 (DATE, 2021)

Paired Training Framework for Time-Constrained Learning. - Jung-Eun Kim; Richard M. Bradford; Max Del Giudice; Zhong Shao 001 (DATE, 2021)

CompCertO: compiling certified open C components. - Jérémie Koenig; Zhong Shao 001 (PLDI, 2021)

Blinder: Partition-Oblivious Hierarchical Scheduling. - Man-Ki Yoon; Mengqi Liu 001; Hao Chen 023; Jung-Eun Kim; Zhong Shao 001 (USENIX Security Symposium, 2021)

Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. - Wolf Honoré; Jieung Kim; Ji-Yong Shin; Zhong Shao 001 (Proc. ACM Program. Lang., 2021)

Verified Compilation of C Programs with a Nominal Memory Model (Artifact). - Yuting Wang 001; Ling Zhang 012; Zhong Shao 001; Jérémie Koenig (Zenodo, 2021)

Verified Compilation of C Programs with a Nominal Memory Model (Artifact). - Yuting Wang 001; Ling Zhang 012; Zhong Shao 001; Jérémie Koenig (Zenodo, 2021)

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 001 (DSN, 2022)

Adore: atomic distributed objects with certified reconfiguration. - Wolf Honoré; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (PLDI, 2022)

Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation. - Mengqi Liu 001; Zhong Shao 001; Hao Chen 023; Man-Ki Yoon; Jung-Eun Kim (Proc. ACM Program. Lang., 2022)

Layered and object-based game semantics. - Arthur Oliveira Vale; Paul-André Melliès; Zhong Shao 001; Jérémie Koenig; Léo Stefanesco (Proc. ACM Program. Lang., 2022)

Verified compilation of C programs with a nominal memory model. - Yuting Wang 001; Ling Zhang 012; Zhong Shao 001; Jérémie Koenig (Proc. ACM Program. Lang., 2022)

A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation. - Ling Zhang 012; Yuting Wang 001; Jérémie Koenig; Zhong Shao 001 (CoRR, 2023)

Ou: Automating the Parallelization of Zero-Knowledge Protocols. - Yuyang Sang; Ning Luo; Samuel Judson; Ben Chaimberg; Timos Antonopoulos; Xiao Wang 012; Ruzica Piskac; Zhong Shao 001 (IACR Cryptol. ePrint Arch., 2023)

A Compositional Theory of Linearizability. - Arthur Oliveira Vale; Zhong Shao 001; Yixuan Chen 002 (Proc. ACM Program. Lang., 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang 012; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Zenodo, 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang 012; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Zenodo, 2023)

A NAND Use Case for Cybersecurity Experiments. - Timothy Fraser; Xuwei Liu; Qingkai Shi; Xiangyu Zhang 001; Mark Wutka; Daniel Balasubramanian; Hao Chen 023; Zhong Shao 001 (SecDev, 2024)

Foundational Verification of Smart Contracts through Verified Compilation. - Vilhelm Sjöberg; Kinnari Dave; Daniel Britten; Maria A Schett; Xinyuan Sun; Qinshi Wang; Sean Noble Anderson; Steve Reeves; Zhong Shao 001 (CoRR, 2024)

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. - Wolf Honoré; Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. - Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Wolf Honoré; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

Compositionality and Observational Refinement for Linearizability with Crashes. - Arthur Oliveira Vale; Zhongye Wang; Yixuan Chen 002; Peixin You; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang 012; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification. - Jieung Kim; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. - Jieung Kim; Jérémie Koenig; Hao Chen 023; Ronghui Gu; Zhong Shao 001 (J. Syst. Archit., 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols. - Longfei Qiu; Jingqi Xiao; Ji-Yong Shin; Zhong Shao 001 (Proc. ACM Program. Lang., 2025)

Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. - Yu Zhang 086; Jérémie Koenig; Zhong Shao 001; Yuting Wang 001 (Proc. ACM Program. Lang., 2025)

CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks. - Ling Zhang 012; Yuting Wang 001; Yalun Liang; Zhong Shao 001 (Proc. ACM Program. Lang., 2025)

CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks. - Ling Zhang 012; Yuting Wang 001; Yalun Liang; Zhong Shao 001 (Zenodo, 2025)