2025
Security Analysis and Formal Verification on Blockchain and its Applications.
,
,
,
,
,
,
,
,
,
,
,
Found. Trends Priv. Secur., 2025
2024
ThreadAbs: A template to build verified thread-local interfaces with software scheduler abstractions.
J. Syst. Archit., February, 2024
SimplMM: A simplified and abstract multicore hardware model for large scale system software formal verification.
J. Syst. Archit., February, 2024
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions.
Proc. ACM Program. Lang., January, 2024
Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2024
2023
Spoq: Scaling Machine-Checkable Systems Verification in Coq.
Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023
2022
Giallar: push-button verification for the qiskit Quantum compiler.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022
DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols.
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022
Design and Verification of the Arm Confidential Compute Architecture.
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022
UPGRADVISOR: Early Adopting Dependency Updates Using Hybrid Program Analysis and Hardware Tracing.
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022
2021
Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version).
CoRR, 2021
SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts.
CoRR, 2021
Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor.
Proceedings of the 30th USENIX Security Symposium, 2021
A Secure and Formally Verified Linux KVM Hypervisor.
Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware.
Proceedings of the SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, 2021
Gleipnir: toward practical error analysis for Quantum programs.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols.
Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021
2020
Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation.
Proc. ACM Program. Lang., 2020
Learning nonlinear loop invariants with gated continuous logic networks.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020
CLN2INV: Learning Loop Invariants with Continuous Logic Networks.
Proceedings of the 8th International Conference on Learning Representations, 2020
2019
Contract-based verification of a realistic quantum compiler.
CoRR, 2019
Building certified concurrent OS kernels.
Commun. ACM, 2019
Using concurrent relational logic with helpers for verifying the AtomFS file system.
Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019
Scaling symbolic evaluation for automated verification of systems code with Serval.
Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019
2018
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers.
J. Autom. Reason., 2018
Certified concurrent abstraction layers.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018
Partial Order Aware Concurrency Sampling.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018
2017
An auditing language for preventing correlated failures in the cloud.
Proc. ACM Program. Lang., 2017
Safety and Liveness of MCS Lock - Layer by Layer.
Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017
2016
End-to-end verification of information-flow security for C and assembly programs.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.
Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016
2015
Deep Specifications and Certified Abstraction Layers.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015