default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDZhong Shao
Person information
- affiliation: Yale University, New Haven, Connecticut, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j32]Arthur Oliveira Vale
, Zhong Shao, Yixuan Chen:
A Compositional Theory of Linearizability. J. ACM 71(2): 14:1-14:107 (2024)- [j31]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: 103046 (2024) - [j30]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: 103049 (2024) - [j29]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): 419-448 (2024) - [j28]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): 1140-1164 (2024) - [j27]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): 2160-2190 (2024) - [i7]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 abs/2405.08348 (2024) - 2023
- [j26]Arthur Oliveira Vale, Zhong Shao, Yixuan Chen:
A Compositional Theory of Linearizability. Proc. ACM Program. Lang. 7(POPL): 1089-1120 (2023) - [c80]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: 534-548 - [i6]Ling Zhang, Yuting Wang, Jérémie Koenig, Zhong Shao:
A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation. CoRR abs/2302.12990 (2023) - [i5]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: 657 (2023) - 2022
- [j25]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): 60-88 (2022) - [j24]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): 1-32 (2022) - [j23]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): 1-31 (2022) - [c79]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: 453-465 - [c78]Wolf Honoré, Ji-Yong Shin, Jieung Kim, Zhong Shao:
Adore: atomic distributed objects with certified reconfiguration. PLDI 2022: 379-394 - 2021
- [j22]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): 1-31 (2021) - [c77]Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao:
Adaptive Generative Modeling in Resource-Constrained Environments. DATE 2021: 62-67 - [c76]Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao:
Paired Training Framework for Time-Constrained Learning. DATE 2021: 591-596 - [c75]Jérémie Koenig, Zhong Shao:
CompCertO: compiling certified open C components. PLDI 2021: 1095-1109 - [c74]Man-Ki Yoon, Mengqi Liu, Hao Chen, Jung-Eun Kim, Zhong Shao:
Blinder: Partition-Oblivious Hierarchical Scheduling. USENIX Security Symposium 2021: 2417-2434 - 2020
- [j21]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): 197:1-197:28 (2020) - [j20]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): 20:1-20:31 (2020) - [c73]Jung-Eun Kim, Richard M. Bradford, Zhong Shao:
AnytimeNet: Controlling Time-Quality Tradeoffs in Deep Neural Network Architectures. DATE 2020: 945-950 - [c72]Jung-Eun Kim, Richard M. Bradford, Man-Ki Yoon, Zhong Shao:
ABC: Abstract prediction Before Concreteness. DATE 2020: 1103-1108 - [c71]Valerie Chen, Man-Ki Yoon, Zhong Shao:
Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems. ICRA 2020: 11060-11066 - [c70]Jérémie Koenig, Zhong Shao:
Refinement-Based Game Semantics for Certified Abstraction Layers. LICS 2020: 633-647
2010 – 2019
- 2019
- [j19]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): 89-99 (2019) - [j18]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): 353-362 (2019) - [j17]Vilhelm Sjöberg, Yuyang Sang, Shu-Chun Weng, Zhong Shao:
DeepSEA: a language for certified system software. Proc. ACM Program. Lang. 3(OOPSLA): 136:1-136:27 (2019) - [j16]Yuting Wang, Pierre Wilke, Zhong Shao:
An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang. 3(POPL): 62:1-62:30 (2019) - [c69]Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao:
Integrating Formal Schedulability Analysis into a Verified OS Kernel. CAV (2) 2019: 496-514 - [c68]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: 299-311 - [c67]Valerie Chen, Man-Ki Yoon, Zhong Shao:
Novelty Detection via Network Saliency in Visual-Based Deep Learning. DSN Workshops 2019: 52-57 - [c66]Man-Ki Yoon, Zhong Shao:
ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems. ICDCS 2019: 1149-1160 - [i4]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 abs/1905.06768 (2019) - [i3]Valerie Chen, Man-Ki Yoon, Zhong Shao:
Novelty Detection via Network Saliency in Visual-based Deep Learning. CoRR abs/1906.03685 (2019) - [i2]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 abs/1911.07726 (2019) - 2018
- [j15]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): 141-189 (2018) - [c65]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: 646-661 - 2017
- [c64]Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao:
Safety and Liveness of MCS Lock - Layer by Layer. APLAS 2017: 273-297 - [c63]Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao:
Automated Resource Analysis with Coq Proof Objects. CAV (2) 2017: 64-85 - 2016
- [c62]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: 653-669 - [c61]Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu:
Toward compositional verification of interruptible OS kernels and device drivers. PLDI 2016: 431-447 - [c60]David Costanzo, Zhong Shao, Ronghui Gu:
End-to-end verification of information-flow security for C and assembly programs. PLDI 2016: 648-664 - 2015
- [j14]Jan Hoffmann, Zhong Shao:
Type-based amortized resource analysis with integers and arrays. J. Funct. Program. 25 (2015) - [c59]Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu:
A Compositional Semantics for Verified Separate Compilation and Linking. CPP 2015: 3-14 - [c58]Zhong Shao:
Clean-Slate Development of Certified OS Kernels. CPP 2015: 95-96 - [c57]Jan Hoffmann, Zhong Shao:
Automatic Static Cost Analysis for Parallel Programs. ESOP 2015: 132-157 - [c56]Quentin Carbonneaux, Jan Hoffmann, Zhong Shao:
Compositional certified resource bounds. PLDI 2015: 467-478 - [c55]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: 595-608 - [i1]Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao:
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports 5(5): 1-23 (2015) - 2014
- [c54]Hongjin Liang, Xinyu Feng, Zhong Shao:
Compositional verification of termination-preserving refinement of concurrent programs. CSL-LICS 2014: 65:1-65:10 - [c53]Jan Hoffmann, Zhong Shao:
Type-Based Amortized Resource Analysis with Integers and Arrays. FLOPS 2014: 152-168 - [c52]Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao:
End-to-end verification of stack-space bounds for C programs. PLDI 2014: 270-281 - [c51]David Costanzo, Zhong Shao:
A Separation Logic for Enforcing Declarative Information Flow Control Policies. POST 2014: 179-198 - [c50]Jinjiang Lei, Zongyan Qiu, Zhong Shao:
Trace-Based Temporal Verification for Message-Passing Programs. TASE 2014: 10-17 - [e5]Zhong Shao:
Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science 8410, Springer 2014, ISBN 978-3-642-54832-1 [contents] - 2013
- [c49]Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao:
Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. CONCUR 2013: 227-241 - [c48]Jan Hoffmann, Michael Marmar, Zhong Shao:
Quantitative Reasoning for Proving Lock-Freedom. LICS 2013: 124-133 - 2012
- [c47]Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi:
Modular Verification of Concurrent Thread Management. APLAS 2012: 315-331 - [c46]David Costanzo, Zhong Shao:
A Case for Behavior-Preserving Actions in Separation Logic. APLAS 2012: 332-349 - [c45]Alexander Vaynberg, Zhong Shao:
Compositional Verification of a Baby Virtual Memory Manager. CPP 2012: 143-159 - [c44]Peter Kazanzides, Yanni Kouskoulas, Anton Deguet, Zhong Shao:
Proving the correctness of concurrent robot software. ICRA 2012: 4718-4723 - [c43]Antonis Stampoulis, Zhong Shao:
Static and user-extensible proof checking. POPL 2012: 273-284 - [c42]Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, Yong Li:
A Structural Approach to Prophecy Variables. TAMC 2012: 61-71 - 2011
- [j13]Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai:
Weak Updates and Separation Logic. New Gener. Comput. 29(1): 3-29 (2011) - [c41]Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, David Costanzo:
CertiKOS: a certified kernel for secure cloud computing. APSys 2011: 3 - [c40]Wei Wang, Zhong Shao, Xinyu Jiang, Yu Guo:
A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. TASE 2011: 125-132 - [e4]Jean-Pierre Jouannaud, Zhong Shao:
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings. Lecture Notes in Computer Science 7086, Springer 2011, ISBN 978-3-642-25378-2 [contents] - 2010
- [j12]Zhong Shao:
Certified software. Commun. ACM 53(12): 56-66 (2010) - [c39]Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang:
Reasoning about Optimistic Concurrency Using a Program Logic for History. CONCUR 2010: 388-402 - [c38]Rodrigo Ferreira, Xinyu Feng, Zhong Shao:
Parameterized Memory Models and Concurrent Separation Logic. ESOP 2010: 267-286 - [c37]Antonis Stampoulis, Zhong Shao:
VeriML: typed computation of logical terms inside a language with effects. ICFP 2010: 333-344
2000 – 2009
- 2009
- [j11]Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong:
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reason. 42(2-4): 301-347 (2009) - [c36]Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai:
Weak updates and separation logic. APLAS 2009: 178-193 - [c35]Zhong Shao:
Modular Development of Certified System Software. TASE 2009: 5 - [e3]Zhong Shao, Benjamin C. Pierce:
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. ACM 2009, ISBN 978-1-60558-379-2 [contents] - 2008
- [c34]Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo:
Certifying low-level programs with hardware interrupts and preemptive threads. PLDI 2008: 170-182 - [c33]Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong:
Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. VSTTE 2008: 54-69 - 2007
- [c32]Xinyu Feng, Rodrigo Ferreira, Zhong Shao:
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. ESOP 2007: 173-188 - [c31]Hongxu Cai, Zhong Shao, Alexander Vaynberg:
Certified self-modifying code. PLDI 2007: 66-77 - [c30]Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li:
A general framework for certifying garbage collectors and their mutators. PLDI 2007: 468-479 - [c29]Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo:
Foundational Typed Assembly Language with Certified Garbage Collection. TASE 2007: 326-338 - [c28]Xinyu Feng, Zhaozhong Ni, Zhong Shao, Yu Guo:
An open framework for foundational proof-carrying code. TLDI 2007: 67-78 - [c27]Zhaozhong Ni, Dachuan Yu, Zhong Shao:
Using XCAP to Certify Realistic Systems Code: Machine Context Management. TPHOLs 2007: 189-206 - [e2]Zhong Shao:
Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings. Lecture Notes in Computer Science 4807, Springer 2007, ISBN 978-3-540-76636-0 [contents] - 2006
- [c26]Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni:
Modular verification of assembly code with stack-based control abstractions. PLDI 2006: 401-414 - [c25]Zhaozhong Ni, Zhong Shao:
Certified assembly programming with embedded code pointers. POPL 2006: 320-333 - 2005
- [j10]Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou:
A type system for certified binaries. ACM Trans. Program. Lang. Syst. 27(1): 1-45 (2005) - [c24]Xinyu Feng, Zhong Shao:
Modular verification of concurrent assembly code with dynamic thread creation and termination. ICFP 2005: 254-267 - 2004
- [j9]Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao:
Building certified libraries for PCC: dynamic storage allocation. Sci. Comput. Program. 50(1-3): 101-127 (2004) - [c23]Dachuan Yu, Zhong Shao:
Verification of safety properties for concurrent assembly code. ICFP 2004: 175-188 - [c22]Nadeem Abdul Hamid, Zhong Shao:
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. TPHOLs 2004: 118-135 - 2003
- [j8]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): 191-229 (2003) - [j7]Stefan Monnier, Zhong Shao:
Inlining as staged computation. J. Funct. Program. 13(3): 647-676 (2003) - [j6]Bratin Saha, Valery Trifonov, Zhong Shao:
Intensional analysis of quantified types. ACM Trans. Program. Lang. Syst. 25(2): 159-209 (2003) - [c21]Christopher League, Zhong Shao, Valery Trifonov:
Precision in Practice: A Type-Preserving Java Compiler. CC 2003: 106-120 - [c20]Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao:
Building Certified Libraries for PCC: Dynamic Storage Allocation. ESOP 2003: 363-379 - [e1]Zhong Shao, Peter Lee:
Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003. ACM 2003, ISBN 1-58113-649-8 [contents] - 2002
- [j5]Christopher League, Zhong Shao, Valery Trifonov:
Type-preserving compilation of Featherweight Java. ACM Trans. Program. Lang. Syst. 24(2): 112-152 (2002) - [c19]Dachuan Yu, Zhong Shao, Valery Trifonov:
Supporting Binary Compatibility with Static Compilation. Java Virtual Machine Research and Technology Symposium 2002: 165-180 - [c18]Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni:
A Syntactic Approach to Foundational Proof-Carrying Code. LICS 2002: 89-100 - [c17]Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou:
A type system for certified binaries. POPL 2002: 217-232 - 2001
- [c16]Stefan Monnier, Bratin Saha, Zhong Shao:
Principled Scavenging. PLDI 2001: 81-91 - [c15]Zhong Shao:
Invited Talk: Towards a Principled Multi-Language Infrastructure. BABEL 2001: 2 - 2000
- [j4]Zhong Shao:
Typed common intermediate format. ACM SIGSOFT Softw. Eng. Notes 25(1): 82 (2000) - [j3]Zhong Shao, Andrew W. Appel:
Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. 22(1): 129-161 (2000) - [c14]Valery Trifonov, Bratin Saha, Zhong Shao:
Fully reflexive intensional type analysis. ICFP 2000: 82-93
1990 – 1999
- 1999
- [c13]Valery Trifonov, Zhong Shao:
Safe and Principled Language Interoperation. ESOP 1999: 128-146 - [c12]Christopher League, Zhong Shao, Valery Trifonov:
Representing Java Classes in a Typed Intermediate Language. ICFP 1999: 183-196 - [c11]Zhong Shao:
Transparent Modules with Fully Syntactic Signatures. ICFP 1999: 220-232 - 1998
- [c10]Zhong Shao:
Typed Cross-Module Compilation. ICFP 1998: 141-152 - [c9]Zhong Shao, Christopher League, Stefan Monnier:
Implementing Typed Intermediate Languages. ICFP 1998: 313-323 - [c8]