VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems.
Proc. ACM Program. Lang., 2025
A Formal Verification Library Design for Behavioral Refinement of CompCert Clight.
IEEE Access, 2025
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs.
Proc. ACM Program. Lang., 2024
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects.
Proc. ACM Program. Lang., 2024
Crellvm: verified credible compilation for LLVM.
,
,
,
,
,
,
,
,
,
,
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018
Taming undefined behavior in LLVM.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017
Lightweight verification of separate compilation.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016