Zhong Shao - RankMe

131 papers A* 27A 22B 12C 1Misc 5Journal 44Unranked 19

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Ringmaster: How to juggle high-throughput host OS system calls from TrustZone TEEs. CoRR Richard Habeeb, Man-Ki Yoon, Hao Chen, Zhong Shao
2025	J	`jnl`	CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks. Proc. ACM Program. Lang. Ling Zhang, Yuting Wang, Yalun Liang, Zhong Shao
2025	A	`conf`	It's a Non-Stop PARTEE! Practical Multi-Enclave Availability Through Partitioning and Asynchrony. ACSAC Richard Habeeb, Hao Chen, Man-Ki Yoon, Zhong Shao
2025	J	`jnl`	LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols. Proc. ACM Program. Lang. Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao
2025	J	`jnl`	Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. Proc. ACM Program. Lang. Yu Zhang, Jérémie Koenig, Zhong Shao, Yuting Wang
2024	J	`jnl`	A Compositional Theory of Linearizability. J. ACM Arthur Oliveira Vale, Zhong Shao, Yixuan Chen
2024	—	`conf`	A NAND Use Case for Cybersecurity Experiments. SecDev Timothy Fraser, Xuwei Liu, Qingkai Shi, Xiangyu Zhang, Mark Wutka, Daniel Balasubramanian, Hao Chen, Zhong Shao
2024	J	`jnl`	AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. Proc. ACM Program. Lang. Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao
2024	J	`jnl`	Compositionality and Observational Refinement for Linearizability with Crashes. Proc. ACM Program. Lang. Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You, Zhong Shao
2024	J	`jnl`	Foundational Verification of Smart Contracts through Verified Compilation. CoRR Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria Anna Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao
2024	J	`jnl`	Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. Proc. ACM Program. Lang. Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao
2024	J	`jnl`	LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. Proc. ACM Program. Lang. Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, Zhong Shao
2024	J	`jnl`	SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification. J. Syst. Archit. Jieung Kim, Ronghui Gu, Zhong Shao
2024	J	`jnl`	ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions. J. Syst. Archit. Jieung Kim, Jérémie Koenig, Hao Chen, Ronghui Gu, Zhong Shao
2023	J	`jnl`	A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation. CoRR Ling Zhang, Yuting Wang, Jérémie Koenig, Zhong Shao
2023	J	`jnl`	A Compositional Theory of Linearizability. Proc. ACM Program. Lang. Arthur Oliveira Vale, Zhong Shao, Yixuan Chen
2023	A*	`conf`	Ou: Automating the Parallelization of Zero-Knowledge Protocols. CCS Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao
2023	J	`jnl`	Ou: Automating the Parallelization of Zero-Knowledge Protocols. IACR Cryptol. ePrint Arch. Yuyang Sang, Ning Luo, Samuel Judson, Ben Chaimberg, Timos Antonopoulos, Xiao Wang, Ruzica Piskac, Zhong Shao
2022	A*	`conf`	Adore: atomic distributed objects with certified reconfiguration. PLDI Wolf Honoré, Ji-Yong Shin, Jieung Kim, Zhong Shao
2022	J	`jnl`	Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation. Proc. ACM Program. Lang. Mengqi Liu, Zhong Shao, Hao Chen, Man-Ki Yoon, Jung-Eun Kim
2022	J	`jnl`	Layered and object-based game semantics. Proc. ACM Program. Lang. Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, Léo Stefanesco
2022	A	`conf`	TimeDice: Schedulability-Preserving Priority Inversion for Mitigating Covert Timing Channels Between Real-time Partitions. DSN Man-Ki Yoon, Jung-Eun Kim, Richard M. Bradford, Zhong Shao
2022	J	`jnl`	Verified compilation of C programs with a nominal memory model. Proc. ACM Program. Lang. Yuting Wang, Ling Zhang, Zhong Shao, Jérémie Koenig
2021	A	`conf`	Adaptive Generative Modeling in Resource-Constrained Environments. DATE Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao
2021	A*	`conf`	Blinder: Partition-Oblivious Hierarchical Scheduling. USENIX Security Symposium Man-Ki Yoon, Mengqi Liu, Hao Chen, Jung-Eun Kim, Zhong Shao
2021	A*	`conf`	CompCertO: compiling certified open C components. PLDI Jérémie Koenig, Zhong Shao
2021	J	`jnl`	Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. Proc. ACM Program. Lang. Wolf Honoré, Jieung Kim, Ji-Yong Shin, Zhong Shao
2021	A	`conf`	Paired Training Framework for Time-Constrained Learning. DATE Jung-Eun Kim, Richard M. Bradford, Max Del Giudice, Zhong Shao
2020	A	`conf`	ABC: Abstract prediction Before Concreteness. DATE Jung-Eun Kim, Richard M. Bradford, Man-Ki Yoon, Zhong Shao
2020	A	`conf`	AnytimeNet: Controlling Time-Quality Tradeoffs in Deep Neural Network Architectures. DATE Jung-Eun Kim, Richard M. Bradford, Zhong Shao
2020	J	`jnl`	CompCertELF: verified separate compilation of C programs into ELF object files. Proc. ACM Program. Lang. Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao
2020	A*	`conf`	Refinement-Based Game Semantics for Certified Abstraction Layers. LICS Jérémie Koenig, Zhong Shao
2020	A*	`conf`	Task-Aware Novelty Detection for Visual-based Deep Learning in Autonomous Systems. ICRA Valerie Chen, Man-Ki Yoon, Zhong Shao
2020	J	`jnl`	Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Proc. ACM Program. Lang. Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon
2019	J	`jnl`	A New Hierarchical Software Architecture Towards Safety-Critical Aspects of a Drone System. CoRR Xiaorui Zhu, Chen Liang, Zhen-guo Yin, Zhong Shao, Meng-qi Liu, Hao Chen
2019	J	`jnl`	A new hierarchical software architecture towards safety-critical aspects of a drone system. Frontiers Inf. Technol. Electron. Eng. Xiaorui Zhu, Chen Liang, Zhen-guo Yin, Zhong Shao, Meng-qi Liu, Hao Chen
2019	A	`conf`	ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems. ICDCS Man-Ki Yoon, Zhong Shao
2019	J	`jnl`	An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang. Yuting Wang, Pierre Wilke, Zhong Shao
2019	J	`jnl`	Building certified concurrent OS kernels. Commun. ACM Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, David Costanzo
2019	J	`jnl`	DeepSEA: a language for certified system software. Proc. ACM Program. Lang. Vilhelm Sjöberg, Yuyang Sang, Shu-Chun Weng, Zhong Shao
2019	—	`conf`	Integrating Formal Schedulability Analysis into a Verified OS Kernel. CAV (2) Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao
2019	—	`conf`	Novelty Detection via Network Saliency in Visual-Based Deep Learning. DSN Workshops Valerie Chen, Man-Ki Yoon, Zhong Shao
2019	J	`jnl`	Novelty Detection via Network Saliency in Visual-based Deep Learning. CoRR Valerie Chen, Man-Ki Yoon, Zhong Shao
2019	J	`jnl`	TaskShuffler++: Real-Time Schedule Randomization for Reducing Worst-Case Vulnerability to Timing Inference Attacks. CoRR Man-Ki Yoon, Jung-Eun Kim, Richard M. Bradford, Zhong Shao
2019	—	`conf`	WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. SoCC Ji-Yong Shin, Jieung Kim, Wolf Honoré, Hernán Vanzetto, Srihari Radhakrishnan, Mahesh Balakrishnan, Zhong Shao
2018	A*	`conf`	Certified concurrent abstraction layers. PLDI Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro
2018	J	`jnl`	Toward Compositional Verification of Interruptible OS Kernels and Device Drivers. J. Autom. Reason. Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
2017	—	`conf`	Automated Resource Analysis with Coq Proof Objects. CAV (2) Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao
2017	B	`conf`	Safety and Liveness of MCS Lock - Layer by Layer. APLAS Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao
2016	A*	`conf`	CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. OSDI Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo
2016	A*	`conf`	End-to-end verification of information-flow security for C and assembly programs. PLDI David Costanzo, Zhong Shao, Ronghui Gu
2016	A*	`conf`	Toward compositional verification of interruptible OS kernels and device drivers. PLDI Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu
2015	B	`conf`	A Compositional Semantics for Verified Separate Compilation and Linking. CPP Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu
2015	A	`conf`	Automatic Static Cost Analysis for Parallel Programs. ESOP Jan Hoffmann, Zhong Shao
2015	B	`conf`	Clean-Slate Development of Certified OS Kernels. CPP Zhong Shao
2015	J	`jnl`	Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
2015	A*	`conf`	Compositional certified resource bounds. PLDI Quentin Carbonneaux, Jan Hoffmann, Zhong Shao
2015	A*	`conf`	Deep Specifications and Certified Abstraction Layers. POPL Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo
2015	J	`jnl`	Type-based amortized resource analysis with integers and arrays. J. Funct. Program. Jan Hoffmann, Zhong Shao
2014	—	`conf`	A Separation Logic for Enforcing Declarative Information Flow Control Policies. POST David Costanzo, Zhong Shao
2014	—	`conf`	Compositional verification of termination-preserving refinement of concurrent programs. CSL-LICS Hongjin Liang, Xinyu Feng, Zhong Shao
2014	A*	`conf`	End-to-end verification of stack-space bounds for C programs. PLDI Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, Zhong Shao
2014	A	`ed.`	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 ESOP Zhong Shao
2014	Misc	`conf`	Trace-Based Temporal Verification for Message-Passing Programs. TASE Jinjiang Lei, Zongyan Qiu, Zhong Shao
2014	Misc	`conf`	Type-Based Amortized Resource Analysis with Integers and Arrays. FLOPS Jan Hoffmann, Zhong Shao
2013	B	`conf`	Characterizing Progress Properties of Concurrent Objects via Contextual Refinements. CONCUR Hongjin Liang, Jan Hoffmann, Xinyu Feng, Zhong Shao
2013	A*	`conf`	Quantitative Reasoning for Proving Lock-Freedom. LICS Jan Hoffmann, Michael Marmar, Zhong Shao
2012	B	`conf`	A Case for Behavior-Preserving Actions in Separation Logic. APLAS David Costanzo, Zhong Shao
2012	C	`conf`	A Structural Approach to Prophecy Variables. TAMC Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, Yong Li
2012	B	`conf`	Compositional Verification of a Baby Virtual Memory Manager. CPP Alexander Vaynberg, Zhong Shao
2012	B	`conf`	Modular Verification of Concurrent Thread Management. APLAS Yu Guo, Xinyu Feng, Zhong Shao, Peizhi Shi
2012	A*	`conf`	Proving the correctness of concurrent robot software. ICRA Peter Kazanzides, Yanni Kouskoulas, Anton Deguet, Zhong Shao
2012	A*	`conf`	Static and user-extensible proof checking. POPL Antonis Stampoulis, Zhong Shao
2011	Misc	`conf`	A Simple Model for Certifying Assembly Programs with First-Class Function Pointers. TASE Wei Wang, Zhong Shao, Xinyu Jiang, Yu Guo
2011	—	`conf`	CertiKOS: a certified kernel for secure cloud computing. APSys Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, David Costanzo
2011	B	`ed.`	Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings CPP Jean-Pierre Jouannaud, Zhong Shao
2011	J	`jnl`	Weak Updates and Separation Logic. New Gener. Comput. Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai
2010	J	`jnl`	Certified software. Commun. ACM Zhong Shao
2010	A	`conf`	Parameterized Memory Models and Concurrent Separation Logic. ESOP Rodrigo Ferreira, Xinyu Feng, Zhong Shao
2010	B	`conf`	Reasoning about Optimistic Concurrency Using a Program Logic for History. CONCUR Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang
2010	A	`conf`	VeriML: typed computation of logical terms inside a language with effects. ICFP Antonis Stampoulis, Zhong Shao
2009	J	`jnl`	Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reason. Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong
2009	Misc	`conf`	Modular Development of Certified System Software. TASE Zhong Shao
2009	A*	`ed.`	Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009 POPL Zhong Shao, Benjamin C. Pierce
2009	B	`conf`	Weak updates and separation logic. APLAS Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai
2008	A*	`conf`	Certifying low-level programs with hardware interrupts and preemptive threads. PLDI Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo
2008	—	`conf`	Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. VSTTE Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong
2007	A*	`conf`	A general framework for certifying garbage collectors and their mutators. PLDI Andrew McCreight, Zhong Shao, Chunxiao Lin, Long Li
2007	—	`conf`	An open framework for foundational proof-carrying code. TLDI Xinyu Feng, Zhaozhong Ni, Zhong Shao, Yu Guo
2007	A*	`conf`	Certified self-modifying code. PLDI Hongxu Cai, Zhong Shao, Alexander Vaynberg
2007	Misc	`conf`	Foundational Typed Assembly Language with Certified Garbage Collection. TASE Chunxiao Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, Yu Guo
2007	A	`conf`	On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. ESOP Xinyu Feng, Rodrigo Ferreira, Zhong Shao
2007	B	`ed.`	Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings APLAS Zhong Shao
2007	—	`conf`	Using XCAP to Certify Realistic Systems Code: Machine Context Management. TPHOLs Zhaozhong Ni, Dachuan Yu, Zhong Shao
2006	A*	`conf`	Certified assembly programming with embedded code pointers. POPL Zhaozhong Ni, Zhong Shao
2006	A*	`conf`	Modular verification of assembly code with stack-based control abstractions. PLDI Xinyu Feng, Zhong Shao, Alexander Vaynberg, Sen Xiang, Zhaozhong Ni
2005	J	`jnl`	A type system for certified binaries. ACM Trans. Program. Lang. Syst. Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou
2005	A	`conf`	Modular verification of concurrent assembly code with dynamic thread creation and termination. ICFP Xinyu Feng, Zhong Shao
2004	J	`jnl`	Building certified libraries for PCC: dynamic storage allocation. Sci. Comput. Program. Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao
2004	—	`conf`	Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. TPHOLs Nadeem Abdul Hamid, Zhong Shao
2004	A	`conf`	Verification of safety properties for concurrent assembly code. ICFP Dachuan Yu, Zhong Shao
2003	J	`jnl`	A Syntactic Approach to Foundational Proof-Carrying Code. J. Autom. Reason. Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
2003	A	`conf`	Building Certified Libraries for PCC: Dynamic Storage Allocation. ESOP Dachuan Yu, Nadeem Abdul Hamid, Zhong Shao
2003	J	`jnl`	Inlining as staged computation. J. Funct. Program. Stefan Monnier, Zhong Shao
2003	J	`jnl`	Intensional analysis of quantified types. ACM Trans. Program. Lang. Syst. Bratin Saha, Valery Trifonov, Zhong Shao
2003	B	`conf`	Precision in Practice: A Type-Preserving Java Compiler. CC Christopher League, Zhong Shao, Valery Trifonov
2003	—	`ed.`	Proceedings of TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, Louisiana, USA, January 18, 2003 TLDI Zhong Shao, Peter Lee
2002	A*	`conf`	A Syntactic Approach to Foundational Proof-Carrying Code. LICS Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
2002	A*	`conf`	A type system for certified binaries. POPL Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos Papaspyrou
2002	—	`conf`	Supporting Binary Compatibility with Static Compilation. Java Virtual Machine Research and Technology Symposium Dachuan Yu, Zhong Shao, Valery Trifonov
2002	J	`jnl`	Type-preserving compilation of Featherweight Java. ACM Trans. Program. Lang. Syst. Christopher League, Zhong Shao, Valery Trifonov
2001	—	`conf`	Invited Talk: Towards a Principled Multi-Language Infrastructure. BABEL Zhong Shao
2001	A*	`conf`	Principled Scavenging. PLDI Stefan Monnier, Bratin Saha, Zhong Shao
2000	J	`jnl`	Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. Zhong Shao, Andrew W. Appel
2000	A	`conf`	Fully reflexive intensional type analysis. ICFP Valery Trifonov, Bratin Saha, Zhong Shao
2000	J	`jnl`	Typed common intermediate format. ACM SIGSOFT Softw. Eng. Notes Zhong Shao
1999	A	`conf`	Representing Java Classes in a Typed Intermediate Language. ICFP Christopher League, Zhong Shao, Valery Trifonov
1999	A	`conf`	Safe and Principled Language Interoperation. ESOP Valery Trifonov, Zhong Shao
1999	A	`conf`	Transparent Modules with Fully Syntactic Signatures. ICFP Zhong Shao
1998	A	`conf`	Implementing Typed Intermediate Languages. ICFP Zhong Shao, Christopher League, Stefan Monnier
1998	—	`conf`	Optimal Type Lifting. Types in Compilation Bratin Saha, Zhong Shao
1998	—	`conf`	Type-Directed Continuation Allocation. Types in Compilation Zhong Shao, Valery Trifonov
1998	A	`conf`	Typed Cross-Module Compilation. ICFP Zhong Shao
1997	A	`conf`	Flexible Representation Analysis. ICFP Zhong Shao
1997	—	`conf`	Typed Common Intermediate Format. DSL Zhong Shao
1996	J	`jnl`	Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures. J. Funct. Program. Andrew W. Appel, Zhong Shao
1995	A*	`conf`	A Type-Based Compiler for Standard ML. PLDI Zhong Shao, Andrew W. Appel
1994	—	`conf`	Space-Efficient Closure Representations. LISP and Functional Programming Zhong Shao, Andrew W. Appel
1994	—	`conf`	Unrolling Lists. LISP and Functional Programming Zhong Shao, John H. Reppy, Andrew W. Appel
1993	A*	`conf`	Smartest Recompilation. POPL Zhong Shao, Andrew W. Appel
1992	J	`jnl`	Callee-Save Registers in Continuation-Passing Style. LISP Symb. Comput. Andrew W. Appel, Zhong Shao