Sotabase

Career

· Professor, Yale Engineering2025–
· Researcher, PostDoc, and PhD Positions, Yale University (Department of Computer Science)2024–
· Faculty Member, Yale School of Medicine2007–
· Professor, Yale University

Publications (135)

This Paper Is Included in the Proceedings of the 12th Usenix Symposium on Operating Systems Design and Implementation (osdi '16). Certikos: an Extensible Architecture for Building Certified Concurrent Os Kernels Certikos: an Extensible Architecture for Building Certified Concurrent Os Kernels
340
cited
Deep Specifications and Certified Abstraction Layers
ACM-SIGACT Symposium on Principles of Programming Languages · 2015
214
cited
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
European Symposium on Programming · 2007
133
cited
A Syntactic Approach to Foundational Proof-Carrying Code
Proceedings 17th Annual IEEE Symposium on Logic in Computer Science · 2002
131
cited
A type-based compiler for standard ML
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 1995
131
cited
Certified assembly programming with embedded code pointers
ACM-SIGACT Symposium on Principles of Programming Languages · 2006
120
cited
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2008
112
cited
Compositional certified resource bounds
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2015
109
cited
Certified self-modifying code
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2007
101
cited
Certified concurrent abstraction layers
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2018
100
cited
Space-efficient closure representations
LFP '94 · 1994
99
cited
Smartest recompilation
ACM-SIGACT Symposium on Principles of Programming Languages · 1993
89
cited
Yale University Department of Computer Science Building Certified Libraries for PCC : Dynamic Storage Allocation
2005
88
cited
Modular verification of assembly code with stack-based control abstractions
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2006
85
cited
End-to-end verification of information-flow security for C and assembly programs
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2016
81
cited
Implementing typed intermediate languages
ACM SIGPLAN International Conference on Functional Programming · 1998
81
cited
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Journal of automated reasoning · 2016
81
cited
A type system for certified binaries
TOPL · 2005
78
cited
An open framework for foundational proof-carrying code
ACM SIGPLAN International Workshop on Types In Languages Design And Implementation · 2007
75
cited
A general framework for certifying garbage collectors and their mutators
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2007
74
cited
Sotabase
Zhong Shao | Researcher Profile | Sotabase | Sotabase