Research

Identify and eliminate security vulnerabilities with proprietary Formal Verification technology

Publications
Corework

Title

Authors

Year

Type

Type Name

Deep Specifications and Certified Abstraction Layers
R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S. Weng, H. Zhang, and Y. Guo
2015
POPL
Heading
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
H. Chen, X. Wu, Z. Shao, J. Lockerman, and R. Gu
2016
PLDI
Heading
End-to-End Verification of Information-Flow Security for C and Assembly Programs
D. Constanzo, Z. Shao, and R. Gu
2016
PLDI
Heading
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, V. Sjoberg, and D. Constanzo
2016
OSDI
Heading
Partial Order Aware Concurrency Sampling
X. Yuan, J. Yang, and R. Gu
2018
CAV
Heading
Certified Concurrent Abstraction Layers
R. Gu, Z. Shao, J. Kim, X. Wu, J. Koenig, V. Sjoberg, H. Chen, D. Constanzo, and T.Ramananandro
2018
PLDI
Heading
DeepSEA: A Language for Certified System Software
V. SJÖBERG, Y. SANG, S. Weng, and Z. Shao
2019
OOPSLA
Heading
Using Concurrent Relational Logic with Helper for Verifying the AtomFS File System
M. Zou, H. Ding, D. Du, M. Fu, R. Gu, and H. Chen
2019
SOSP
Heading
Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval
L. Nelson, J. Bornholt, R. Gu, A. Baumann, E. Torlak, and X. Wang
2019
SOSP
Heading
Building Certified Concurrent OS Kernels
R. Gu, Z. Shao, H. Chen, J. Kim, J. Koenig, X. Wu, V. Sjoberg, and D. Constanzo
2019
CACM
Heading
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
M. Liu, L. Rieg, Z. Shao, R. Gu, D. Costanzo, J. Kim, and M. Yoon
2020
POPL
Heading
CLN2INV: Learning Loop Invariants with Continuous Logic Networks
R. Gu, S. Jana, J. Wong, G. Ryan, J. Yao
2020
ICLR
Heading
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks
R. Gu, S. Jana, J. Wong, G. Ryan, J. Yao
2020
PLDI
Heading

Corework

Lorem ipsum dolor sit amet, consectetur adipiscing elit. Suspendisse varius enim in eros elementum tristique. Duis cursus, mi quis viverra ornare, eros dolor interdum nulla, ut commodo diam libero vitae erat. Aenean faucibus nibh et justo cursus id rutrum lorem imperdiet. Nunc ut sem vitae risus tristique posuere.

Write Verified Smart Contracts with DeepSea

CertiK is developing the DeepSEA programming language, which eases the work on verification by automatically generating executable code, as well as a formal model that can be loaded into the Coq theorem prover. The model is output as a functional program with a higher level of abstraction and in the style of abstraction layers.

DeepSea Language Manual

[A short description of what the document contains]

Download Compiler

[A short description of what the document contains]

Download GitHub

Download GitHub

Facebook’s “Move” Programming Language: How Does It Compare to Solidity and DeepSEA?

Introducing NoOps: The New Way to Run Your Nodes

CertiK’s Audit of the Torus Distributed Key Generation Protocol

Subscribe to our Newsletter

Subscribe

  • Be the first to know about our product and service updates

  • Read our experts' analysis on the latest blockchain news

  • Be notified of our community events and get connected to people like you