Zhong Shao

ORCID

Publication Activity (10 Years)

Years Active: 1992-2024
Publications (10 Years): 46

Top Venues

Proc. ACM Program. Lang.

PLDI

CoRR

DATE

Publications

Jieung Kim, Jérémie Koenig, Hao Chen, Ronghui Gu, Zhong Shao
ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. J. Syst. Archit. 147 (2024)
Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, Zhong Shao
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Arthur Oliveira Vale, Zhong Shao, Yixuan Chen
A Compositional Theory of Linearizability. J. ACM 71 (2) (2024)
Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao
Foundational Verification of Smart Contracts through Verified Compilation. CoRR (2024)
Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. Proc. ACM Program. Lang. 8 (POPL) (2024)
Jieung Kim, Ronghui Gu, Zhong Shao
SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification. J. Syst. Archit. 147 (2024)
Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. Proc. ACM Program. Lang. 8 (OOPSLA1) (2024)
Ling Zhang, Yuting Wang, Jérémie Koenig, Zhong Shao
A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation. CoRR (2023)
Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao
Ou: Automating the Parallelization of Zero-Knowledge Protocols. IACR Cryptol. ePrint Arch. 2023 (2023)
Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao
Ou: Automating the Parallelization of Zero-Knowledge Protocols. CCS (2023)
Arthur Oliveira Vale, Zhong Shao, Yixuan Chen
A Compositional Theory of Linearizability. Proc. ACM Program. Lang. 7 (POPL) (2023)
Yuting Wang, Ling Zhang, Zhong Shao, Jérémie Koenig
Verified compilation of C programs with a nominal memory model. Proc. ACM Program. Lang. 6 (POPL) (2022)
Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, Jung-Eun Kim
Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Wolf Honoré, Ji-Yong Shin, Jieung Kim, Zhong Shao
Adore: atomic distributed objects with certified reconfiguration. PLDI (2022)
Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, Léo Stefanesco
Layered and object-based game semantics. Proc. ACM Program. Lang. 6 (POPL) (2022)
Man-Ki Yoon, Jung-Eun Kim, Richard M. Bradford, Zhong Shao
TimeDice: Schedulability-Preserving Priority Inversion for Mitigating Covert Timing Channels Between Real-time Partitions. DSN (2022)
Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao
Paired Training Framework for Time-Constrained Learning. DATE (2021)
Jérémie Koenig, Zhong Shao
CompCertO: compiling certified open C components. PLDI (2021)
Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao
Adaptive Generative Modeling in Resource-Constrained Environments. DATE (2021)
Wolf Honoré, Jieung Kim, Ji-Yong Shin, Zhong Shao
Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Man-Ki Yoon, Mengqi Liu, Hao Chen, Jung-Eun Kim, Zhong Shao
Blinder: Partition-Oblivious Hierarchical Scheduling. USENIX Security Symposium (2021)
Jung-Eun Kim, Richard M. Bradford, Man-Ki Yoon, Zhong Shao
ABC: Abstract prediction Before Concreteness. DATE (2020)
Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao
CompCertELF: verified separate compilation of C programs into ELF object files. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Jérémie Koenig, Zhong Shao
Refinement-Based Game Semantics for Certified Abstraction Layers. LICS (2020)
Jung-Eun Kim, Richard M. Bradford, Zhong Shao
AnytimeNet: Controlling Time-Quality Tradeoffs in Deep Neural Network Architectures. DATE (2020)
Valerie Chen, Man-Ki Yoon, Zhong Shao
Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems. ICRA (2020)
Valerie Chen, Man-Ki Yoon, Zhong Shao
Novelty Detection via Network Saliency in Visual-Based Deep Learning. DSN Workshops (2019)
Ji-Yong Shin, Jieung Kim, Wolf Honoré, Hernán Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, Zhong Shao
WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. SoCC (2019)
Ji-Yong Shin, Jieung Kim, Hernán Vanzetto, Srihari Radhakrishnan, Wolf Honoré, Zhong Shao, Mahesh Balakrishnan
WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. SoCC (2019)
Xiaorui Zhu, Chen Liang, Zhen-guo Yin, Zhong Shao, Meng-qi Liu, Hao Chen
A New Hierarchical Software Architecture Towards Safety-Critical Aspects of a Drone System. CoRR (2019)
Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao
Integrating Formal Schedulability Analysis into a Verified OS Kernel. CAV (2) (2019)
Valerie Chen, Man-Ki Yoon, Zhong Shao
Novelty Detection via Network Saliency in Visual-based Deep Learning. CoRR (2019)
Man-Ki Yoon, Jung-Eun Kim, Richard M. Bradford, Zhong Shao
TaskShuffler++: Real-Time Schedule Randomization for Reducing Worst-Case Vulnerability to Timing Inference Attacks. CoRR (2019)
Vilhelm Sjöberg, Yuyang Sang, Shu-Chun Weng, Zhong Shao
DeepSEA: a language for certified system software. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, David Costanzo
Building certified concurrent OS kernels. Commun. ACM 62 (10) (2019)
Yuting Wang, Pierre Wilke, Zhong Shao
An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang. 3 (POPL) (2019)
Xiaorui Zhu, Chen Liang, Zhen-guo Yin, Zhong Shao, Meng-qi Liu, Hao Chen
A new hierarchical software architecture towards safety-critical aspects of a drone system. Frontiers Inf. Technol. Electron. Eng. 20 (3) (2019)
Man-Ki Yoon, Zhong Shao
ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems. ICDCS (2019)
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. J. Autom. Reason. 61 (1-4) (2018)
Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro
Certified concurrent abstraction layers. PLDI (2018)
Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao
Automated Resource Analysis with Coq Proof Objects. CAV (2) (2017)
Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao
Safety and Liveness of MCS Lock - Layer by Layer. APLAS (2017)
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
Toward compositional verification of interruptible OS kernels and device drivers. PLDI (2016)
David Costanzo, Zhong Shao, Ronghui Gu
End-to-end verification of information-flow security for C and assembly programs. PLDI (2016)
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. OSDI (2016)
Jan Hoffmann, Zhong Shao
Type-based amortized resource analysis with integers and arrays. J. Funct. Program. 25 (2015)
Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports 5 (5) (2015)
Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo
Deep Specifications and Certified Abstraction Layers. POPL (2015)
Zhong Shao
Clean-Slate Development of Certified OS Kernels. CPP (2015)
Jan Hoffmann, Zhong Shao
Automatic Static Cost Analysis for Parallel Programs. ESOP (2015)
Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu
A Compositional Semantics for Verified Separate Compilation and Linking. CPP (2015)
Quentin Carbonneaux, Jan Hoffmann, Zhong Shao
Compositional certified resource bounds. PLDI (2015)
Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao
End-to-end verification of stack-space bounds for C programs. PLDI (2014)
Jan Hoffmann, Zhong Shao
Type-Based Amortized Resource Analysis with Integers and Arrays. FLOPS (2014)
Hongjin Liang, Xinyu Feng, Zhong Shao
Compositional verification of termination-preserving refinement of concurrent programs. CSL-LICS (2014)
Jinjiang Lei, Zongyan Qiu, Zhong Shao
Trace-Based Temporal Verification for Message-Passing Programs. TASE (2014)
David Costanzo, Zhong Shao
A Separation Logic for Enforcing Declarative Information Flow Control Policies. POST (2014)
Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. CONCUR (2013)
Jan Hoffmann, Michael Marmar, Zhong Shao
Quantitative Reasoning for Proving Lock-Freedom. LICS (2013)
Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi
Modular Verification of Concurrent Thread Management. APLAS (2012)
Alexander Vaynberg, Zhong Shao
Compositional Verification of a Baby Virtual Memory Manager. CPP (2012)
Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, Yong Li
A Structural Approach to Prophecy Variables. TAMC (2012)
Peter Kazanzides, Yanni Kouskoulas, Anton Deguet, Zhong Shao
Proving the correctness of concurrent robot software. ICRA (2012)
Antonis Stampoulis, Zhong Shao
Static and user-extensible proof checking. POPL (2012)
David Costanzo, Zhong Shao
A Case for Behavior-Preserving Actions in Separation Logic. APLAS (2012)
Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai
Weak Updates and Separation Logic. New Gener. Comput. 29 (1) (2011)
Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, David Costanzo
CertiKOS: a certified kernel for secure cloud computing. APSys (2011)
Wei Wang, Zhong Shao, Xinyu Jiang, Yu Guo
A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. TASE (2011)
Rodrigo Ferreira, Xinyu Feng, Zhong Shao
Parameterized Memory Models and Concurrent Separation Logic. ESOP (2010)
Zhong Shao
Certified software. Commun. ACM 53 (12) (2010)
Antonis Stampoulis, Zhong Shao
VeriML: typed computation of logical terms inside a language with effects. ICFP (2010)
Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang
Reasoning about Optimistic Concurrency Using a Program Logic for History. CONCUR (2010)
Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reason. 42 (2-4) (2009)
Zhong Shao
Modular Development of Certified System Software. TASE (2009)
Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai
Weak updates and separation logic. APLAS (2009)
Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. VSTTE (2008)
Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo
Certifying low-level programs with hardware interrupts and preemptive threads. PLDI (2008)
Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo
Foundational Typed Assembly Language with Certified Garbage Collection. TASE (2007)
Xinyu Feng, Rodrigo Ferreira, Zhong Shao
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. ESOP (2007)
Zhaozhong Ni, Dachuan Yu, Zhong Shao
Using XCAP to Certify Realistic Systems Code: Machine Context Management. TPHOLs (2007)
Hongxu Cai, Zhong Shao, Alexander Vaynberg
Certified self-modifying code. PLDI (2007)
Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li
A general framework for certifying garbage collectors and their mutators. PLDI (2007)
Xinyu Feng, Zhaozhong Ni, Zhong Shao, Yu Guo
An open framework for foundational proof-carrying code. TLDI (2007)
Zhaozhong Ni, Zhong Shao
Certified assembly programming with embedded code pointers. POPL (2006)
Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni
Modular verification of assembly code with stack-based control abstractions. PLDI (2006)
Xinyu Feng, Zhong Shao
Modular verification of concurrent assembly code with dynamic thread creation and termination. ICFP (2005)
Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou
A type system for certified binaries. ACM Trans. Program. Lang. Syst. 27 (1) (2005)
Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao
Building certified libraries for PCC: dynamic storage allocation. Sci. Comput. Program. 50 (1-3) (2004)
Nadeem Abdul Hamid, Zhong Shao
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. TPHOLs (2004)
Dachuan Yu, Zhong Shao
Verification of safety properties for concurrent assembly code. ICFP (2004)
Bratin Saha, Valery Trifonov, Zhong Shao
Intensional analysis of quantified types. ACM Trans. Program. Lang. Syst. 25 (2) (2003)
Christopher League, Zhong Shao, Valery Trifonov
Precision in Practice: A Type-Preserving Java Compiler. CC (2003)
Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao
Building Certified Libraries for PCC: Dynamic Storage Allocation. ESOP (2003)
Stefan Monnier, Zhong Shao
Inlining as staged computation. J. Funct. Program. 13 (3) (2003)
Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
A Syntactic Approach to Foundational Proof-Carrying Code. J. Autom. Reason. 31 (3-4) (2003)
Dachuan Yu, Zhong Shao, Valery Trifonov
Supporting Binary Compatibility with Static Compilation. Java Virtual Machine Research and Technology Symposium (2002)
Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
A Syntactic Approach to Foundational Proof-Carrying Code. LICS (2002)
Christopher League, Zhong Shao, Valery Trifonov
Type-preserving compilation of Featherweight Java. ACM Trans. Program. Lang. Syst. 24 (2) (2002)
Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou
A type system for certified binaries. POPL (2002)

Zhong Shao.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Zhong Shao