Sotabase

Career

· Tang Family Associate Professor of Computer Science, Columbia University2024–
· Tang Family Assistant Professor, Columbia University2021–2023
· Co-founder, CertiK2018–
· Assistant Professor, Columbia University2018–2020
· Associate Research Scientist, Columbia University2018–2018
· Software Engineer, Google2016–2017
· PhD in Computer Science, Yale University2013–2016
· Research Assistant, Yale University2012–2016
· M.Phil. in Computer Science, Yale University2011–2013
· B.S. in Computer Science with Highest Distinction, Tsinghua University2007–2011

Publications (31)

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
Scaling symbolic evaluation for automated verification of systems code with Serval
Symposium on Operating Systems Principles · 2019
118
cited
Certified concurrent abstraction layers
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2018
100
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
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Journal of automated reasoning · 2016
81
cited
CLN2INV: Learning Loop Invariants with Continuous Logic Networks
International Conference on Learning Representations · 2019
68
cited
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
USENIX Symposium on Operating Systems Design and Implementation · 2021
68
cited
A Secure and Formally Verified Linux KVM Hypervisor
IEEE Symposium on Security and Privacy · 2021
66
cited
Learning nonlinear loop invariants with gated continuous logic networks
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2020
62
cited
DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols
USENIX Symposium on Operating Systems Design and Implementation · 2022
44
cited
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware
Symposium on Operating Systems Principles · 2021
43
cited
Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor
USENIX Security Symposium · 2021
42
cited
Using concurrent relational logic with helpers for verifying the AtomFS file system
Symposium on Operating Systems Principles · 2019
42
cited
Building certified concurrent OS kernels
Communications of the ACM · 2019
41
cited
Partial Order Aware Concurrency Sampling
International Conference on Computer Aided Verification · 2018
35
cited
Giallar: push-button verification for the qiskit Quantum compiler
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2022
34
cited
Safety and Liveness of MCS Lock - Layer by Layer
Asian Symposium on Programming Languages and Systems · 2017
28
cited
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation
Proc. ACM Program. Lang. · 2019
25
cited
Gleipnir: toward practical error analysis for Quantum programs
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2021
20
cited
Sotabase
Ronghui Gu | Researcher Profile | Sotabase | Sotabase