Registered user since Sun 28 Sep 2014
Contributions
2022
PLDI
- (PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
- Islaris: Verification of Machine Code Against Authoritative ISA Semantics
- RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
- Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
- (PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types
PLDI 2022-profile
View general profile
View general profile